def ud.succ_inj
import bend-osdev-u32@0.1.0.0/PROOF_div.bend as PROOFDivimport Base
25def ud.succ_inj(+x: Nat, +y: Nat, e: {1n+x == 1n+y : Nat}) -> {x == y : Nat}:
26 Equal.cong(Nat, Nat, ud.pred, 1n+x, 1n+y, e)
import bend-osdev-u32@0.1.0.0/PROOF_div.bend as PROOFDivimport Base
25def ud.succ_inj(+x: Nat, +y: Nat, e: {1n+x == 1n+y : Nat}) -> {x == y : Nat}:
26 Equal.cong(Nat, Nat, ud.pred, 1n+x, 1n+y, e)