U32.injective: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U32
Lines 45-56 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&start_line=45&end_line=56

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

def injective(+a: U32, +b: U32, +e: {U32.to_nat(a) == U32.to_nat(b) : Nat}) -> {a == b : U32}:
  match a b:
    case U32{+x} U32{+y}:
      Equal.cong(Word(32n), U32, w => U32{w}, x, y,
        Equal.trans(Word(32n), x, S.from_nat(32n, S.unsigned(32n, x)), y,
          Equal.sym(Word(32n), S.from_nat(32n, S.unsigned(32n, x)), x, word_from_unsigned(x)),
          Equal.trans(Word(32n), S.from_nat(32n, S.unsigned(32n, x)), S.from_nat(32n, S.unsigned(32n, y)), y,
            Equal.cong(Nat, Word(32n), v => S.from_nat(32n, v), S.unsigned(32n, x), S.unsigned(32n, y),
              Equal.trans(Nat, S.unsigned(32n, x), U32.to_nat(U32{x}), S.unsigned(32n, y),
                Equal.sym(Nat, U32.to_nat(U32{x}), S.unsigned(32n, x), to_nat_word(x)),
                Equal.trans(Nat, U32.to_nat(U32{x}), U32.to_nat(U32{y}), S.unsigned(32n, y), e, to_nat_word(y)))),
            word_from_unsigned(y))))

Uses (11):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=unsigned
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=to_nat_word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=word_from_unsigned