law dbl_dist

lawful-words@0.1.0.0 · proof_nat.bend:501

import Base

501law dbl_dist:
502  for +x: Nat
503  for +y: Nat
504  {Nat.double(Nat.add(x, y)) == Nat.add(Nat.double(x), Nat.double(y)) : Nat}