def leaf_value

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
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

142def leaf_value(-T: Data, +y: T, +j: Nat, +x: T, +hj: {Nat.is_lt(j, 1n) == True{} : Bool}, +hx: {SC.nth(T, Con{y, Nil{}}, j) == Some{x} : Maybe<&2, T>}) -> {y == x : T}:
143  match j:
144    case 0n:
145      L.some_inj(T, y, x, hx)
146    case 1n+q:
147      Empty.absurd({y == x : T}, N.lt_zero_absurd(q, hj))