def uq.succ_cong

bend-osdev-algo@0.1.0.0 · proof_u32.bend:56

import Base

56def uq.succ_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
57  %e : {1n+a == 1n+_ : Nat}
58  {==}