def uniq

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:55

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

55# r1 + 2^n x == r2 + 2^n y with both r below 2^n forces r1 == r2
56def 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}:
57  A.uniq(n, r1, r2, x, y, h, lt1(n, one, h1, r1, b1), lt1(n, one, h1, r2, b2))