def AP.pred_cong

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

import Base

1336def AP.pred_cong(-a: Nat, -b: Nat, e: {1n+a == 1n+b : Nat}) -> {a == b : Nat}:
1337  Equal.cong(Nat, Nat, n => AP.pred(n), 1n+a, 1n+b, e)