= Solution
The empty-<list> case uses $f(a)=b$. At a cons, assuming the equality for the tail, the calculation is
$$
f(\operatorname{foldr}\ g\ a\ (x:xs))=f(g\ x\ (\operatorname{foldr}\ g\ a\ xs))=h\ x\ (f(\operatorname{foldr}\ g\ a\ xs))=h\ x\ (\operatorname{foldr}\ h\ b\ xs).
$$
The middle equality is the supplied compatibility condition, instantiated with the folded tail; the last expression is the <right fold> on the whole <list>. <Structural induction> therefore proves fusion for finite total spines.
The strictness condition accounts for a bottom-valued input spine: the inner <list fold> returns bottom, and $f(\bot)=\bot$ makes the two sides agree. The same <induction> covers finite <partial lists>. For pure definable continuous <functions>, an infinite <list> is the limit of its finite partial approximations, so equality extends to it. These are the three distinct obligations in the <right-fold fusion law>; strictness is not needed if the domain is restricted to finite terminating spines.
Back to article page
