Array.freeze_thaw: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend as Array
Lines 88-95 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&start_line=88&end_line=95

import Base

def freeze_thaw(-T: Data, +t: Tree<T>) -> {freeze(T, thaw(T, t)) == t : Tree<T>}:
  match t:
    case TLeaf{x}:
      {==}
    case TNode{+l, +r}:
      %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>}
      %Equal.sym(Tree<T>, freeze(T, thaw(T, r)), r, freeze_thaw(T, r)) : {TNode{l, _} == TNode{l, r} : Tree<T>}
      {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=freeze
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=thaw