def wr.d6

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:281

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

281def wr.d6(+x0: Nat) -> {x0 == Nat.mul(1n, x0) : Nat}:
282  %Equal.sym(Nat, x0, Nat.mul(1n, x0), Equal.sym(Nat, Nat.mul(1n, x0), x0, UL.nat_one_mul(x0))) : {_ == Nat.mul(1n, x0) : Nat}
283  {==}