def ur.r33

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

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

1704def ur.r33(+x0: Nat) -> {x0 == Nat.mul(1n, x0) : Nat}:
1705  %Equal.sym(Nat, x0, Nat.mul(1n, x0), Equal.sym(Nat, Nat.mul(1n, x0), x0, Laws.nat_one_mul(x0))) : {_ == Nat.mul(1n, x0) : Nat}
1706  {==}