def at_val

bend-collections-laws-math@1.0.0.0 · proofs/math/number/fixprime.bend:76

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

76# an unwrapped candidate sits at its value
77def at_val(+m: U32, +t: Nat, +ht: {Nat.add(v(m), C.shift(32n, 0n)) == t : Nat}) -> {v(m) == t : Nat}:
78  Equal.trans(Nat, v(m), Nat.add(v(m), 0n), t, Equal.sym(Nat, Nat.add(v(m), 0n), v(m), N.add_zero(v(m))), ht)