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

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

def sequence_storage(-Element: Data,-length: Nat,-values: List<&2,Element>,
  evidence: SequenceEvidence<Element,length,values>) -> Tree.Tree<Element>:
  SequenceEvidence{storage,contents,room} = evidence
  storage

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=SequenceEvidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree