def un.succ_cong

bend-osdev-u32@0.1.0.0 · PROOF.bend:51

import Base

51def un.succ_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
52  %e : {1n+a == 1n+_ : Nat}
53  {==}