We want to prove

.L1:List (rev(rev(L1)) = L1)

- Base case : prove assertion for
L1 = nil - Show
rev(rev(nil)) = nil

- Show
- Induction case : prove assertion for
L1 = cons(M,L) L1 = L - Introduce the
lemma L1,L2:List (rev(append(L1,L2)) = append(rev(L2), rev(L1))) - Change hypothesis
L1,L2:List (rev(append(L1,L2)) = append(rev(L2), rev(L1))) - Quantifier elimination introduces new
constants *m :Nat*and*l :List*. - Implication elimination assumes
rev(rev(l)) = l - Change hypothesis
rev(rev(l)) = l - Show
rev(rev(cons(m,l))) = cons(m,l)

- Introduce the