law from_nat_add

lawful-words@0.1.0.0 · proof_u32.bend:460

import Base

460law from_nat_add:
461  for +x: Nat
462  for +y: Nat
463  {U32.from_nat(Nat.add(x, y)) == U32.add(U32.from_nat(x), U32.from_nat(y)) : U32}