def ur.r32

bend-osdev-u32@0.1.0.0 · PROOF.bend:1700

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as Laws

1700def ur.r32(+x0: Nat) -> {Nat.mul(1n, x0) == x0 : Nat}:
1701  %Equal.sym(Nat, Nat.mul(1n, x0), x0, Laws.nat_one_mul(x0)) : {_ == x0 : Nat}
1702  {==}