def AP.succ_cong

bend-osdev-array@0.1.0.1 · PROOF.bend:46

import Base

46def AP.succ_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
47  %e : {1n+a == 1n+_ : Nat}
48  {==}