law succ_inj

lawful-words@0.1.0.0 · proof_nat.bend:133

import Base

133law succ_inj:
134  for +a: Nat
135  for +b: Nat
136  for e: {1n+a == 1n+b : Nat}
137  {a == b : Nat}