Natural-number fold fusion law ($f\circ \mathrm{foldNat}(g,a)=\mathrm{foldNat}(h,b)$)

Suppose $f$ is a strict function, $f(a)=b$ and $f\circ g=h\circ f$. The zero case of the asserted equation is the base identity; the successor case rewrites $f(g(z))$ as $h(f(z))$ and applies structural induction. At an undefined argument, the strict function premise makes both sides the bottom value. For pure definable Haskell functions, equality on finite partial approximations extends to infinite constructor chains by continuity in the information order. For finite total arguments alone, the zero and successor proof does not require strictness.