def eqm_of

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/step.bend:176

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

176def eqm_of(+k: Nat, +v: Nat, +x: Nat, +e: {v == C.low(k, x) : Nat}) -> {C.low(k, v) == C.low(k, x) : Nat}:
177  Equal.trans(Nat, C.low(k, v), C.low(k, C.low(k, x)), C.low(k, x), Equal.cong(Nat, Nat, z => C.low(k, z), v, C.low(k, x), e), low_low(k, x))