Clone.second_equal: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
Lines 58-65 of bendtorch-core@0.1.0.0/src/storage/clone.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&start_line=58&end_line=65

import Base

def second_equal(-T: Data, -d: Nat, -original: Array<T>, cloned: Cloned<T, d, original>) ->
  {Pair.snd(Array<T>, Array<T>, Array.clone(T, original)) == original : Array<T>}:
  match cloned:
    case Cloned{first, second, exact, same_first, same_second, valid_first, valid_second}:
      Equal.trans(Array<T>, Pair.snd(Array<T>, Array<T>, Array.clone(T, original)), second, original,
        Equal.cong(Array<T> & Array<T>, Array<T>, r => Pair.snd(Array<T>, Array<T>, r),
          Array.clone(T, original), (first, second),
          Equal.sym(Array<T> & Array<T>, (first, second), Array.clone(T, original), exact)), same_second)

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=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=Cloned