StorageRefinement.reflect_packed: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
Lines 11-22 of stelliferous@0.0.2.0/proofs/storage_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&start_line=11&end_line=22

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

# The tree model covers every native Array owner, including capacities larger
# than its logical sequence. These equalities allocate no runtime conversion.
def reflect_packed(-Element: Data,+tree: Tree.Tree<Element>) ->
  {Tree.reflect(Element,Tree.pack(Element,tree)) == tree : Tree.Tree<Element>}:
  match tree:
    case Tree.Leaf{value}: {==}
    case Tree.Node{+left,+right}:
      %Equal.sym(Tree.Tree<Element>,Tree.reflect(Element,Tree.pack(Element,left)),left,reflect_packed(Element,left)) :
        {Tree.Node{_,Tree.reflect(Element,Tree.pack(Element,right))} == Tree.Node{left,right} : Tree.Tree<Element>}
      %Equal.sym(Tree.Tree<Element>,Tree.reflect(Element,Tree.pack(Element,right)),right,reflect_packed(Element,right)) :
        {Tree.Node{left,_} == Tree.Node{left,right} : Tree.Tree<Element>}
      {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=reflect