def mv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:519

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/u64laws.bend as LW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

519def mv(+k: Nat, +hk: {k == 64n : Nat}, +m: WU.U64, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}) -> {Nat.is_lt(1n+mp, C.pow2(k)) == True{} : Bool}:
520  L.subst(Nat, z => {Nat.is_lt(z, C.pow2(k)) == True{} : Bool}, v(m), 1n+mp, hm, LW.val_lt(k, hk, m))