law add_self_r

lawful-words@0.1.0.0 · proof_nat.bend:303

import Base

303# x + y = x gives y = 0.
304law add_self_r:
305  for +x: Nat
306  for +y: Nat
307  for e: {Nat.add(x, y) == x : Nat}
308  {y == 0n : Nat}