def succ_inj

import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as Nat

import Base

17def succ_inj(+a: Nat, +b: Nat, e: {1n+a == 1n+b : Nat}) -> {a == b : Nat}:
18  Equal.cong(Nat, Nat, pred, 1n+a, 1n+b, e)

Uses (3)