Structural Induction for Lists
lLet P be a property of (open) lists
l
lTo show
("L) P(L)

lit is sufficient to show:
lP([]) // Basis
l("L) ("A)  P(L) => P([A | L]) // Induction step