def uq.double_cong

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

import Base

60def uq.double_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {Nat.double(a) == Nat.double(b) : Nat}:
61  %e : {Nat.double(a) == Nat.double(_) : Nat}
62  {==}