PROOF.full_t: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/PROOF.bend as PROOF
Lines 14-18 of lawful-arrays@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&start_line=14&end_line=18

import Base
import lawful-arrays@0.1.0.0/defs.bend as D
import lawful-arrays@0.1.0.0/proof_base.bend as B
import lawful-arrays@0.1.0.0/proof_tree.bend as P

# Rewrites a fact about a into the same fact about the mirror.
def full_t(-T: Data, -a: Array<T>, -t: P.Tree<T>, +d: Nat, e: {P.fromT(T, t) == a : Array<T>},
  hf: {D.full(T, a, d) == True{} : Bool}) -> {D.full(T, P.fromT(T, t), d) == True{} : Bool}:
  B.subst(Array<T>, x => {D.full(T, x, d) == True{} : Bool}, a, P.fromT(T, t),
    Equal.sym(Array<T>, P.fromT(T, t), a, e), hf)

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/defs.bend&name=full
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=fromT