def un.double_cong

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

import Base

58def un.double_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {Nat.double(a) == Nat.double(b) : Nat}:
59  %e : {Nat.double(a) == Nat.double(_) : Nat}
60  {==}