def second_equal
bendtorch-core@0.1.0.0 · src/storage/clone.bend:58
import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
import Base
58def second_equal(-T: Data, -d: Nat, -original: Array<T>, cloned: Cloned<T, d, original>) ->
59 {Pair.snd(Array<T>, Array<T>, Array.clone(T, original)) == original : Array<T>}:
60 match cloned:
61 case Cloned{first, second, exact, same_first, same_second, valid_first, valid_second}:
62 Equal.trans(Array<T>, Pair.snd(Array<T>, Array<T>, Array.clone(T, original)), second, original,
63 Equal.cong(Array<T> & Array<T>, Array<T>, r => Pair.snd(Array<T>, Array<T>, r),
64 Array.clone(T, original), (first, second),
65 Equal.sym(Array<T> & Array<T>, (first, second), Array.clone(T, original), exact)), same_second)