def AP.double_cong

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

import Base

50def AP.double_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {Nat.double(a) == Nat.double(b) : Nat}:
51  %e : {Nat.double(a) == Nat.double(_) : Nat}
52  {==}