law one_mul

lawful-arrays@0.1.0.0 · proof_index.bend:332

import Base

332law one_mul:
333  for +x: Nat
334  {Nat.mul(U32.to_nat(1), x) == x : Nat}