StorageRefinement.pack_reflected: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
Lines 24-33 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=24&end_line=33

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

def pack_reflected(-Element: Data,storage: Array<Element>) ->
  {Tree.pack(Element,Tree.reflect(Element,storage)) == storage : Array<Element>}:
  match storage:
    case ALeaf{value}: {==}
    case ANode{left,right}:
      %pack_reflected(Element,left) :
        {ANode{Tree.pack(Element,Tree.reflect(Element,left)),Tree.pack(Element,Tree.reflect(Element,right))} == ANode{_,right} : Array<Element>}
      %pack_reflected(Element,right) :
        {ANode{Tree.pack(Element,Tree.reflect(Element,left)),Tree.pack(Element,Tree.reflect(Element,right))} == ANode{Tree.pack(Element,Tree.reflect(Element,left)),_} : Array<Element>}
      {==}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  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