StorageRefinement.Observation: type of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
Lines 439-443 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=439&end_line=443

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

# Reify an affine owner once for proof consumers that need both its Data model
# and the relation. This helper is never imported by a numerical runtime path.
type Observation<-Element: Data,-storage: Array<Element>> is Data:
  Observation{tree: Tree.Tree<Element>,packed: {Tree.pack(Element,tree) == storage : Array<Element>},
    reflected: {tree == Tree.reflect(Element,storage) : Tree.Tree<Element>}}

Uses (4):
  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=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