def eqm_of

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/impl.bend:22

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/math/random/pcg/step.bend as ST

22def eqm_of(+v: Nat, +x: Nat, +e: {v == C.low(64n, x) : Nat}) -> {C.low(64n, v) == C.low(64n, x) : Nat}:
23  ST.eqm_of(64n, v, x, e)