def nth0_upd_same

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/words32.bend:68

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

68def nth0_upd_same(+xs: List<&2, U32>, +i: Nat, +v: U32, +h: {Nat.is_lt(i, SC.length(U32, xs)) == True{} : Bool}) -> {nth0(SC.update(U32, xs, i, v), i) == v : U32}:
69  match xs i:
70    case Nil{} _:
71      Empty.absurd({nth0(SC.update(U32, Nil{}, i, v), i) == v : U32}, N.lt_zero_absurd(i, h))
72    case Con{x, t} 0n:
73      {==}
74    case Con{x, t} 1n+p:
75      nth0_upd_same(t, p, v, h)