def mv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:518

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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32P

518def mv(+k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}) -> {Nat.is_lt(1n+mp, C.pow2(k)) == True{} : Bool}:
519  L.subst(Nat, z => {Nat.is_lt(z, C.pow2(k)) == True{} : Bool}, v(m), 1n+mp, hm, U32P.val_lt(1n, {==}, k, hk, m))