def AP.get_same_array.go
bend-osdev-array@0.1.0.1 · PROOF.bend:730
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
730def AP.get_same_array.go(-T: Data, -a: Array<T>, +i: U32, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Pair.fst(Array<T>, T, Array.get(T, a, i)) == a : Array<T>}:
731 (t, e) = r
732 %e : {Pair.fst(Array<T>, T, Array.get(T, _, i)) == _ : Array<T>}
733 %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), AP.get_top(T, t, i)), AP.get_top_eq(T, t, i)) : {Pair.fst(Array<T>, T, _) == AP.build(T, t) : Array<T>}
734 {==}