def leaf_update

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:135

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

135def leaf_update(-T: Data, +x: T, +v: T, +j: Nat, +hj: {Nat.is_lt(j, 1n) == True{} : Bool}) -> {Con{v, Nil{}} == SC.update(T, Con{x, Nil{}}, j, v) : List<&2, T>}:
136  match j:
137    case 0n:
138      {==}
139    case 1n+q:
140      Empty.absurd({Con{v, Nil{}} == Con{x, Nil{}} : List<&2, T>}, N.lt_zero_absurd(q, hj))