ProofShift.ws.uniq: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/proof_shift.bend as ProofShift
Lines 299-309 of bend-osdev-word64@0.1.1.0/proof_shift.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&start_line=299&end_line=309

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/proof_value.bend as P
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

# x, y < 2^n and x + 2^n p = y + 2^n q: x = y
def ws.uniq(+n: Nat, p: Nat, q: Nat, +x: Nat, +y: Nat, e: {Nat.add(x, U.U32Nat.dbl(n, p)) == Nat.add(y, U.U32Nat.dbl(n, q)) : Nat}, hx: {Nat.is_lt(x, U.U32Nat.dbl(n, 1n)) == True{} : Bool}, hy: {Nat.is_lt(y, U.U32Nat.dbl(n, 1n)) == True{} : Bool}) -> {x == y : Nat}:
  match p q:
    case 0n 0n:
      Equal.trans(Nat, x, Nat.add(x, U.U32Nat.dbl(n, 0n)), y, Equal.sym(Nat, Nat.add(x, U.U32Nat.dbl(n, 0n)), x, ns.d0(n, x)), Equal.trans(Nat, Nat.add(x, U.U32Nat.dbl(n, 0n)), Nat.add(y, U.U32Nat.dbl(n, 0n)), y, e, ns.d0(n, y)))
    case 0n 1n+ +q:
      Empty.absurd({x == y : Nat}, P.wn.lt_irrefl(x, P.wn.lt_rw2(x, Nat.add(y, U.U32Nat.dbl(n, 1n+q)), x, Equal.trans(Nat, Nat.add(y, U.U32Nat.dbl(n, 1n+q)), Nat.add(x, U.U32Nat.dbl(n, 0n)), x, Equal.sym(Nat, Nat.add(x, U.U32Nat.dbl(n, 0n)), Nat.add(y, U.U32Nat.dbl(n, 1n+q)), e), ns.d0(n, x)), UO.nat_lt_le_trans(x, U.U32Nat.dbl(n, 1n+q), Nat.add(y, U.U32Nat.dbl(n, 1n+q)), UO.nat_lt_le_trans(x, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+q), hx, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+q)), Nat.is_le(1n, 1n+q), True{}, UL.dbl_le(n, 1n, 1n+q), P.wn.le_zero(q))), UL.nat_le_add(U.U32Nat.dbl(n, 1n+q), y)))))
    case 1n+ +p 0n:
      Empty.absurd({x == y : Nat}, P.wn.lt_irrefl(y, P.wn.lt_rw2(y, Nat.add(x, U.U32Nat.dbl(n, 1n+p)), y, Equal.trans(Nat, Nat.add(x, U.U32Nat.dbl(n, 1n+p)), Nat.add(y, U.U32Nat.dbl(n, 0n)), y, e, ns.d0(n, y)), UO.nat_lt_le_trans(y, U.U32Nat.dbl(n, 1n+p), Nat.add(x, U.U32Nat.dbl(n, 1n+p)), UO.nat_lt_le_trans(y, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+p), hy, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+p)), Nat.is_le(1n, 1n+p), True{}, UL.dbl_le(n, 1n, 1n+p), P.wn.le_zero(p))), UL.nat_le_add(U.U32Nat.dbl(n, 1n+p), x)))))
    case 1n+ +p 1n+ +q:
      ws.uniq(n, p, q, x, y, UL.nat_add_cancel(U.U32Nat.dbl(n, 1n), Nat.add(x, U.U32Nat.dbl(n, p)), Nat.add(y, U.U32Nat.dbl(n, q)), Equal.trans(Nat, Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(x, U.U32Nat.dbl(n, p))), Nat.add(x, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), UL.nat_add_left_comm(U.U32Nat.dbl(n, 1n), x, U.U32Nat.dbl(n, p)), Equal.trans(Nat, Nat.add(x, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p))), Nat.add(x, U.U32Nat.dbl(n, 1n+p)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), Equal.cong(Nat, Nat, v => Nat.add(x, v), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)), U.U32Nat.dbl(n, 1n+p), Equal.sym(Nat, U.U32Nat.dbl(n, 1n+p), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)), UL.dbl_add(n, 1n, p))), Equal.trans(Nat, Nat.add(x, U.U32Nat.dbl(n, 1n+p)), Nat.add(y, U.U32Nat.dbl(n, 1n+q)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), e, Equal.trans(Nat, Nat.add(y, U.U32Nat.dbl(n, 1n+q)), Nat.add(y, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), Equal.cong(Nat, Nat, v => Nat.add(y, v), U.U32Nat.dbl(n, 1n+q), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q)), UL.dbl_add(n, 1n, q)), UL.nat_add_left_comm(y, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q))))))), hx, hy)

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_le
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_left_comm
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_le_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS_order.bend&name=nat_lt_le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.d0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.le_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.lt_irrefl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.lt_rw2