 Right-fold fusion law

If $f$ is strict, $f(a)=b$, and $f(g(x,y))=h(x,f(y))$, then $f\circ \mathrm{foldr}(g,a)=\mathrm{foldr}(h,b)$. The empty case uses the base image and the cons case uses compatibility followed by structural induction. Strictness handles a bottom-valued spine. For pure definable continuous functions, equality on finite partial lists extends to infinite lists by finite approximation. For finite total inputs alone, induction does not require the strictness hypothesis.