= 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 \i[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.<Haskell 2010 Language Report>[§3.1, Errors, and §3.17.2, Informal Semantics of Pattern Matching]{ref}
Back to article page
