Wide.join: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as Wide
Lines 103-105 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&start_line=103&end_line=105

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend as NM

# Exact limb boundary used by the host bridge; limbs themselves are primitive U32.
def join(n: Nat, +m: Nat, a: Word(n), b: Word(m)) -> Word(Nat.add(n, m)):
  NM.join(n, m, a, b)

Uses (4):
  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=Word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend&name=join