law mul_one

lawful-words@0.1.0.0 · proof_nat.bend:427

import Base

427law mul_one:
428  for +a: Nat
429  {Nat.mul(a, 1n) == a : Nat}