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

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

def lift_pair_observation(~Element: Data,~Context: Data,
  ~Proposition: Context -> @-input: Array<Element> -> @-output: Array<Element> ->
    @-input_tree: Tree.Tree<Element> -> @-output_tree: Tree.Tree<Element> -> Type,
  +context: Context,-input: Array<Element>,-output: Array<Element>,
  input_observation: Observation<Element,input>,output_observation: Observation<Element,output>,
  canonical: @+input_tree: Tree.Tree<Element> -> @+output_tree: Tree.Tree<Element> ->
    Proposition(context,Tree.pack(Element,input_tree),Tree.pack(Element,output_tree),input_tree,output_tree)) ->
  Proposition(context,input,output,Tree.reflect(Element,input),Tree.reflect(Element,output)):
  Observation{+input_tree,input_packed,input_reflected} = input_observation
  Observation{+output_tree,output_packed,output_reflected} = output_observation
  %input_reflected : Proposition(context,input,output,_,Tree.reflect(Element,output))
  %output_reflected : Proposition(context,input,output,input_tree,_)
  %input_packed : Proposition(context,_,output,input_tree,output_tree)
  %output_packed : Proposition(context,Tree.pack(Element,input_tree),_,input_tree,output_tree)
  canonical(input_tree)(output_tree)

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_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