ProofGen.add_cancel_l: law of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 850-855 of minebender-game@1.0.0.0/proof_gen.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_gen.bend&start_line=850&end_line=855

import Base

law add_cancel_l:
  for +c: Nat
  for +a: Nat
  for +b: Nat
  for e: {Nat.add(c, a) == Nat.add(c, b) : Nat}
  {a == b : Nat}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=succ_inj