 Solution

For finite lists, use structural induction: establish P []; then, for arbitrary x and xs, assume P xs and prove P (x:xs). The induction hypothesis must quantify over any other parameters that need to change in the step.

For all Haskell list values, finite terminating spines are insufficient: also establish P undefined, and allow arbitrary, possibly undefined, heads in the cons step. This proves the equation for finite partial lists ending in the bottom value. An infinite lazy list is the limit of these finite approximations. Equations between pure definable computable functions are preserved by those limits, so the equation extends to infinite inputs. This last argument requires that admissibility property; an arbitrary logical property of lists need not have it. The distinction between [] and the bottom value is essential.^[ref]