def succ_injective

bendtorch-core@0.1.0.0 · src/shape/unique_proofs.bend:20

import Base

20def succ_injective(-a: Nat, -b: Nat, equal: {1n+a == 1n+b : Nat}) -> {a == b : Nat}:
21  Equal.cong(Nat, Nat, pred, 1n+a, 1n+b, equal)