def un.dd1
bend-osdev-u32@0.1.0.0 · PROOF.bend:523
import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base
523def un.dd1(+r: Nat, +d: Nat, +a: Nat, +b: Nat, e: {Nat.add(r, d) == 1n+Nat.add(a, b) : Nat}) -> {Nat.add(Nat.double(r), Nat.double(d)) == 2n+Nat.add(Nat.double(a), Nat.double(b)) : Nat}:
524 Equal.trans(Nat, Nat.add(Nat.double(r), Nat.double(d)), Nat.double(Nat.add(r, d)), 2n+Nat.add(Nat.double(a), Nat.double(b)), Equal.sym(Nat, Nat.double(Nat.add(r, d)), Nat.add(Nat.double(r), Nat.double(d)), un.double_add(r, d)), Equal.trans(Nat, Nat.double(Nat.add(r, d)), Nat.double(1n+Nat.add(a, b)), 2n+Nat.add(Nat.double(a), Nat.double(b)), un.double_cong(Nat.add(r, d), 1n+Nat.add(a, b), e), un.succ_cong(1n+Nat.double(Nat.add(a, b)), 1n+Nat.add(Nat.double(a), Nat.double(b)), un.succ_cong(Nat.double(Nat.add(a, b)), Nat.add(Nat.double(a), Nat.double(b)), un.double_add(a, b)))))