law dbl_add

lawful-words@0.1.0.0 · proof_nat.bend:488

import Base

488law dbl_add:
489  for +x: Nat
490  {Nat.double(x) == Nat.add(x, x) : Nat}