Solution
= Solution
For two <proper lazy lists>, `twiddle` alternates heads, swapping which <list> is served after each output. Thus both input positions have finite waiting time. A tempting extension is `remalldups . foldr twiddle []`, but arbitrary empty rows make that insufficient: for `[ [1,2] ] ++ repeat []`, it emits `1` and then demands the combination of infinitely many empty rows before it can return to `2`.
Use <diagonal merging of lazy lists> to avoid that obstruction. Maintain a finite active collection, add at most one new row per round, and take one head from every nonempty active row. The supplied `twiddle` combines those singleton contributions into a finite batch:
``
union' = remalldups . rounds []
rounds [] [] = []
rounds active [] = emit active []
rounds active (row:rows) = emit (active ++ [row]) rows
emit active rows = batch ++ rounds tails rows
where (batch, tails) = sweep active
sweep [] = ([], [])
sweep ([]:rows) = sweep rows
sweep ((x:xs):rows) = (twiddle [x] heads, xs:tails)
where (heads, tails) = sweep rows
``
Here `rounds` takes the finite active collection first and the not-yet-introduced outer <list> second. Because `heads` is a finite <list>, `twiddle [x] heads` emits `x` followed by those heads; the finite batch is then completely consumed before the next round. Empty exhausted rows are removed by `sweep`. No step tries to combine infinitely many not-yet-introduced rows.
Index rows and positions from zero. Row $i$ is introduced in round $i$ and contributes its element $j$ in round $i+j$, if that element exists. Every earlier round inspects only finitely many rows. Therefore every occurrence has a finite emission time, proving <fair enumeration>. Applying <first-occurrence duplicate removal> gives
$$
\boxed{\operatorname{union}'=\operatorname{remalldups}\circ\text{finite-round diagonal enumeration}.}
$$
All outer and inner spines must be <proper lazy lists> and <equality tests> must terminate. Infinitely many empty rows after the final contribution still prevent certifying a terminating empty tail, just as part (c) predicts. Undefined input spines have the separate <partial-list interleaving obstruction>; the construction makes no promise to bypass them.