def Mirror
import lawful-arrays@0.1.0.0/proof_tree.bend as ProofTreeimport Base
24def Mirror(-T: Data, -a: Array<T>) -> Data:
25 Sigma<&2, &2, Tree<T>, t => {fromT(T, t) == a : Array<T>}>
import lawful-arrays@0.1.0.0/proof_tree.bend as ProofTreeimport Base
24def Mirror(-T: Data, -a: Array<T>) -> Data:
25 Sigma<&2, &2, Tree<T>, t => {fromT(T, t) == a : Array<T>}>