Hello all, My copy of HS: The Craft Of FP just arrived and I was reading section 8.5 about induction. On page 141, Simon Thompson gives a method of proving properties of functions on lists: 1) Prove that the property holds for the null list 2) Prove that the property holds for (x:xs) under the assumption that the property holds for xs. My question is this: what is the proof of (P([]) and ( P(xs) => P(x:xs))) => P(xs)? In other words, how does proof of the property on empty lists and proof that the property holds on (x:xs) under the assumption that it holds on xs give proof that it holds on all lists? Isn't there a recursive dependency here? You are defining the proof for lists with at least one element based on the assumption that it holds for all lists, right? How does this get you a proof of the general property if it depends on the assumption of the general property? Regards and thanks, Echo Nolan.