StorageRefinement.get_go: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
Lines 113-118 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=113&end_line=118

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

law get_go:
  for -T: Data
  for +tree: Tree.Tree<T>
  for +n: U32
  for +i: U32
  {Array.get.go(T,Tree.pack(T,tree),n,i,U32.is_lt(i,U32.shr(n))) == (Tree.pack(T,tree),Tree.fetch(T,tree,n,i)) : Array<T> & T}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=get_node
  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=fetch
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=pack