def freeze_thaw

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:88

import Base

88def freeze_thaw(-T: Data, +t: Tree<T>) -> {freeze(T, thaw(T, t)) == t : Tree<T>}:
89  match t:
90    case TLeaf{x}:
91      {==}
92    case TNode{+l, +r}:
93      %Equal.sym(Tree<T>, freeze(T, thaw(T, l)), l, freeze_thaw(T, l)) : {TNode{_, freeze(T, thaw(T, r))} == TNode{l, r} : Tree<T>}
94      %Equal.sym(Tree<T>, freeze(T, thaw(T, r)), r, freeze_thaw(T, r)) : {TNode{l, _} == TNode{l, r} : Tree<T>}
95      {==}