page 3  1 2 3 x 
We want to prove
( L1 : List ) rev(rev(L1)) = L1 .We use induction on L1 to prove this goal. For this, we use the induction scheme based on the signature { nil, cons } for List. Induction requires that we do the following:
And thus the main goal is proved. 
Explanation
The main point of note about this proof is that the lemma that it uses was discovered from the failed direct attempt for the original goal in our previous proofweb for the same result. Note that, as on the previous proofpage, the associativity lemma is used in
an implicit way, as an attribute of append.

