def first_equal
bendtorch-core@0.1.0.0 · src/storage/clone.bend:49
import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
import Base
49def first_equal(-T: Data, -d: Nat, -original: Array<T>, cloned: Cloned<T, d, original>) ->
50 {Pair.fst(Array<T>, Array<T>, Array.clone(T, original)) == original : Array<T>}:
51 match cloned:
52 case Cloned{first, second, exact, same_first, same_second, valid_first, valid_second}:
53 Equal.trans(Array<T>, Pair.fst(Array<T>, Array<T>, Array.clone(T, original)), first, original,
54 Equal.cong(Array<T> & Array<T>, Array<T>, r => Pair.fst(Array<T>, Array<T>, r),
55 Array.clone(T, original), (first, second),
56 Equal.sym(Array<T> & Array<T>, (first, second), Array.clone(T, original), exact)), same_first)