law add_cancel_l

lawful-words@0.1.0.0 · proof_nat.bend:274

import Base

274# a + x = a + y gives x = y.
275law add_cancel_l:
276  for +a: Nat
277  for +x: Nat
278  for +y: Nat
279  for e: {Nat.add(a, x) == Nat.add(a, y) : Nat}
280  {x == y : Nat}