Associativity of Append Function

We want to prove

L1,L2,L3:List (append(append(L1, L2), L3) = append(L1, append(L2, L3))) .
We use induction on List to prove this goal. For this, we use the induction scheme based on signature {nil, cons} for List . Induction requires that we do the following:

This page was generated
by Kumo on Mon Jun 01 16:18:55 PDT 1998