First note that in the syntax of the list spec that we are given, the
one element list
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
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
The second proof page of the current proofweb shows
a first attempt to prove the above lemma.