def as_of

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

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