def as_of

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

import Base
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

44# x is the WU.U64 of its value
45def as_of(+x: WU.U64, +n: Nat, +h: {v(x) == n : Nat}) -> {x == of(n) : WU.U64}:
46  Equal.trans(WU.U64, x, of(v(x)), of(n), Equal.sym(WU.U64, of(v(x)), x, LW.rt(x)), Equal.cong(Nat, WU.U64, t => of(t), v(x), n, h))