PROOF.un.dd1: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 523-524 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=523&end_line=524

import Base

def 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}:
  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)))))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.double_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.double_cong
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.succ_cong