def wn.succ_cong

bend-osdev-word64@0.1.1.0 · proof_value.bend:66

import Base

66def wn.succ_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
67  %e : {1n+a == 1n+_ : Nat}
68  {==}