Explanation
First note that in the syntax of the list spec that we are given, the
one element list [n0] appears
as cons(n0, nil) . If we
write the two terms that we need to be equal in order to complete the proof as
an equation using the simpler notation, with · as append, then we get
rev(rev(L1) · [n0]) = [n0] · L1 ,
To prove this, it would suffice, given the inductive hypothesis (which the
proof page also conveniently displays for us) to know the following more
symmetrical result,
rev(L1 · [n0]) = [n0] · rev(L1) .
Although we could prove and then use this, we might as well it generalize to
rev(L1 · L2) = rev(L2) · rev(L1) ,
which is itself an interesting result about reversing lists.
It is now reasonable to hope that proving the above first as a lemma will
allow us to prove our original goal. That this is so is demonstrated in our
second proofweb.
The second proof page of the current proofweb shows
a first attempt to prove the above lemma.
