law succ_inj

lawful-arrays@0.1.0.0 · proof_base.bend:91

import Base

91law succ_inj:
92  for -a: Nat
93  for -b: Nat
94  for e: {1n+a == 1n+b : Nat}
95  {a == b : Nat}