~/jendhub

def get_set_same.go

lawful-arrays@0.1.0.0 · PROOF.bend:116

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

116def get_set_same.go(-T: Data, -a: Array<T>, +i: U32, +v: T, m: P.Mirror(T, a)) ->
117  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}:
118  (t, e) = m
119  %e : {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, _, i, v), i)) == v : T}
120  P.get_set_same_t(T, t, i, v)

Uses (8)

Used by (1)