law succ_inj

minebender-game@1.0.0.0 · proof_base.bend:625

import Base

625law succ_inj:
626  for +a: Nat
627  for +b: Nat
628  for e: {1n+a == 1n+b : Nat}
629  {a == b : Nat}