StorageWitness.clone: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_witness.bend as StorageWitness
Lines 208-222 of stelliferous@0.0.2.0/proofs/storage_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&start_line=208&end_line=222

import Base

# The native clone duplicates payload ownership, while its source observation
# and balance depth are unchanged. This theorem is consumed only by rewrites.
def clone(-Element: Data,+depth: Nat,-storage: Array<Element>,witness: Witness(Element,depth,storage)) ->
  {Array.clone(Element,storage) == (storage,storage) : Array<Element> & Array<Element>}:
  match depth witness:
    case 0n Leaf{value,owner}:
      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) : {Array.clone(Element,_) == (_,_) : Array<Element> & Array<Element>}
      {==}
    case 1n+ +rest Node{left,right,owner,left_balanced,right_balanced}:
      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : {Array.clone(Element,_) == (_,_) : Array<Element> & Array<Element>}
      %Equal.sym(Array<Element> & Array<Element>,Array.clone(Element,left),(left,left),clone(Element,rest,left,left_balanced)) :
        {Array.clone.node(Element,_,Array.clone(Element,right)) == (ANode{left,right},ANode{left,right}) : Array<Element> & Array<Element>}
      %Equal.sym(Array<Element> & Array<Element>,Array.clone(Element,right),(right,right),clone(Element,rest,right,right_balanced)) :
        {Array.clone.node(Element,(left,left),_) == (ANode{left,right},ANode{left,right}) : Array<Element> & Array<Element>}
      {==}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone.node
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=LeafWitness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=NodeWitness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness