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

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

def observed_node(-Element: Data,-left: Array<Element>,-right: Array<Element>,
  left_observation: Observation<Element,left>,right_observation: Observation<Element,right>) -> Observation<Element,ANode{left,right}>:
  Observation{+left_tree,left_packed,left_reflected} = left_observation
  Observation{+right_tree,right_packed,right_reflected} = right_observation
  Observation{Tree.Node{left_tree,right_tree},observed_node_equation(Element,left,right,left_tree,right_tree,left_packed,right_packed),
    observed_node_reflection(Element,left,right,left_tree,right_tree,left_reflected,right_reflected)}

Uses (5):
  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_refinement.bend&name=Observation
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=observed_node_equation
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=observed_node_reflection
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree