PROOF.un.sh: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 526-528 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=526&end_line=528

import Base

# 1 + (2A + (1 + 2B)) = 2 + (2A + 2B)
def un.sh(+a: Nat, +b: Nat) -> {2n+Nat.add(Nat.double(a), Nat.double(b)) == 1n+Nat.add(Nat.double(a), 1n+Nat.double(b)) : Nat}:
  un.succ_cong(1n+Nat.add(Nat.double(a), Nat.double(b)), Nat.add(Nat.double(a), 1n+Nat.double(b)), Equal.sym(Nat, Nat.add(Nat.double(a), 1n+Nat.double(b)), 1n+Nat.add(Nat.double(a), Nat.double(b)), un.add_succ(Nat.double(a), Nat.double(b))))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.succ_cong