Clone.first_equal: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
Lines 49-56 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=49&end_line=56

import Base

def first_equal(-T: Data, -d: Nat, -original: Array<T>, cloned: Cloned<T, d, original>) ->
  {Pair.fst(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.fst(Array<T>, Array<T>, Array.clone(T, original)), first, original,
        Equal.cong(Array<T> & Array<T>, Array<T>, r => Pair.fst(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_first)

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.fst
  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