= Solution
Use <structural induction> on the first finite outer <list> `xss`, with the assertion quantified over every finite `yss`. For `xss = []`, both sides are `[]`. For the nonempty case of <structural induction>, write `xss = xs:xss'`. If `yss = []`, both sides again truncate to `[]`. Otherwise write `yss = ys:yss'`. Expanding the definitions gives
$$
\begin{aligned}
&\operatorname{combine}(\operatorname{map}(z:)(xs:xss'))(ys:yss')\\
&\quad=((z:xs)\mathbin{++}ys):\operatorname{combine}(\operatorname{map}(z:)xss')yss'\\
&\quad=(z:(xs\mathbin{++}ys)):\operatorname{map}(z:)(\operatorname{combine}xss'\,yss')\\
&\quad=\operatorname{map}(z:)\big((xs\mathbin{++}ys):\operatorname{combine}xss'\,yss'\big)\\
&\quad=\operatorname{map}(z:)(\operatorname{combine}(xs:xss')(ys:yss')).
\end{aligned}
$$
The second equality uses the defining equation for <list concatenation> and the <induction hypothesis> for the smaller outer <list> `xss'`. The argument covers unequal outer lengths because the empty second <list> was handled explicitly. Hence
$$
\boxed{\operatorname{combine}(\operatorname{map}(z:)xss)yss
=\operatorname{map}(z:)(\operatorname{combine}xss\,yss).}
$$
Back to article page
