def get_kept.go

lawful-arrays@0.1.0.0 · PROOF.bend:87

import Base
import lawful-arrays@0.1.0.0/proof_tree.bend as P

87def get_kept.go(-T: Data, -a: Array<T>, +i: U32, m: P.Mirror(T, a)) ->
88  {Pair.fst(Array<T>, T, Array.get(T, a, i)) == a : Array<T>}:
89  (t, e) = m
90  %e : {Pair.fst(Array<T>, T, Array.get(T, _, i)) == _ : Array<T>}
91  Equal.cong(Array<T> & T, Array<T>, p => Pair.fst(Array<T>, T, p), Array.get(T, P.fromT(T, t), i),
92    (P.fromT(T, t), Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t), i))), P.get_pair_t(T, t, i))