StorageCloneCertificate.clone: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_clone_certificate.bend as StorageCloneCertificate
Lines 9-14 of stelliferous@0.0.2.0/proofs/storage_clone_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_clone_certificate.bend&start_line=9&end_line=14

import Base
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

def clone(~Element: Data,-input: Array<Element>,evidence: Certificate.Certificate<Element,input>,left: Certificate.Certificate<Element,input>,right: Certificate.Certificate<Element,input>) ->
  Copies<Element,Array.clone(Element,input)>:
  Certificate.Certificate{+depth,equation} = evidence
  %Equal.sym(Array<Element> & Array<Element>,Array.clone(Element,input),(input,input),
    Witness.clone(Element,depth,input,Certificate.witness_at(Element,depth,input,equation))) : Copies<Element,_>
  Copies{left,right}

Uses (9):
  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=Equal.sym
  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_certificate.bend&name=Certificate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=witness_at
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_clone_certificate.bend&name=Copies
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=clone