 Solution

Let $P(zss)$ mean concat (map f zss) = f (concat zss). We use structural induction on lazy lists, including the bottom value and allowing arbitrary, possibly partial, inner lists.

For [], the left side is [] and the right side is f [] = []. For the bottom value $\perp$, both map f and concat are strict functions in the outer spine, and the supplied strictness of $f$ makes the right side $f\perp =\perp$ too.

For the cons case, assume $P(zss)$ and write the new head as xs. The defining equations and the induction hypothesis giveThe third equality is exactly the supplied list concatenation preservation law. No inspection of xs was required, so the argument includes partial inner lists and undefined elements.

This proves the identity for every finite outer spine ending in either [] or $\perp$. In the usual pure Haskell semantics, these functions are Scott continuous maps. An infinite outer list is obtained as a limit by finite approximation of a lazy list; both composite functions preserve that limit. Equality on all its finite approximations therefore gives equality on the infinite outer list. Equivalently, $P$ is an admissible predicate on lazy lists. ConsequentlyThe continuity assumption is the usual semantic assumption for definable functions here; an extension from finite to infinite inputs cannot be justified by ordinary finite induction alone.