Certificates.clone_second: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
Lines 26-31 of bendtorch-core@0.1.0.0/src/storage/certificates.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/certificates.bend&start_line=26&end_line=31

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone

def clone_second(-T: Data, +d: Nat, original: Array<T>, -result: Array<T> & Array<T>,
  equal: {result == Array.clone(T, original) : Array<T> & Array<T>},
  valid: Model.Balanced(T, d, original)) -> Model.Balanced(T, d, Pair.snd(Array<T>, Array<T>, result)):
  %Equal.sym(Array<T> & Array<T>, result, Array.clone(T, original), equal) :
    Model.Balanced(T, d, Pair.snd(Array<T>, Array<T>, _))
  Clone.second_balanced(T, d, original, Clone.certify(T, d, original, valid))

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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=certify
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=second_balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced