StorageBufferModel.packed_contents: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_buffer_model.bend as StorageBufferModel
Lines 134-136 of stelliferous@0.0.2.0/proofs/storage_buffer_model.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&start_line=134&end_line=136

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

def packed_contents(~Element: Data,+model: Model<Element>) -> {contents(~Element,pack(~Element,model)) == content(~Element,model) : Content<Element>}:
  Model{+tree,+length,certificate} = model
  Equal.cong(Tree.Tree<Element>,Content<Element>,tree => Content{tree,length},Tree.reflect(Element,Tree.pack(Element,tree)),tree,StorageLaws.reflect_packed(Element,tree))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=Content
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=Model
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=content
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=contents
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=reflect_packed
  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