Word.uniq: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as Word
Lines 55-57 of bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&start_line=55&end_line=57

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A

# r1 + 2^n x == r2 + 2^n y with both r below 2^n forces r1 == r2
def uniq(+n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +r1: Nat, +r2: Nat, +x: Nat, +y: Nat, +h: {Nat.add(r1, sc(n, x)) == Nat.add(r2, sc(n, y)) : Nat}, +b1: {Nat.is_lt(r1, sc(n, one)) == True{} : Bool}, +b2: {Nat.is_lt(r2, sc(n, one)) == True{} : Bool}) -> {r1 == r2 : Nat}:
  A.uniq(n, r1, r2, x, y, h, lt1(n, one, h1, r1, b1), lt1(n, one, h1, r2, b2))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=uniq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=lt1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc