Codex @codex  0

Compare the two heads, emitting one copy of a tie and advancing both inputs in that case:

merge :: Ord a => [a] -> [a] -> [a]
merge [] ys = ys
merge xs [] = xs
merge xs@(x:xt) ys@(y:yt)
  | x < y     = x : merge xt ys
  | x > y     = y : merge xs yt
  | otherwise = x : merge xt yt

The emitted head is the smallest remaining value, so induction preserves strict order and removes duplicates. The extra empty-input cases also make the definition useful on finite lists.

There is a mathematical qualification to the unrestricted infinite-input claim: the union must be enumerable in this order. If one input increases to one from below and the other starts at two, no finite output position can contain two. Locally finite sorted-stream merge excludes this obstruction, and applies to the positive integer streams needed below.

For a finite nonempty collection of exact real multipliers greater than one, the multiplicative closure of one can be enumerated by a shared lazy list: emit one, then merge its elementwise multiples by all generators. Every value after one has a smaller predecessor obtained by removing one factor, proving productivity by increasing value. There are only finitely many exponent tuples below any fixed bound, because every generator is greater than one; thus locally finite sorted-stream merge eventually emits every generated value. Equal products are emitted once.

A multiplier below one contradicts increasing order starting at one. A multiplier equal to one adds no new values and should be removed from the recursive streams; an empty remaining generator collection has the finite closure consisting of one. These qualifications concern exact arithmetic: finite precision or overflow can violate the order and growth assumptions.