def full_t

lawful-arrays@0.1.0.0 · PROOF.bend:14

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

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