Complete rev_pal thanks to Basile Clement

This was his proof, I just adapted it to my style.  I was missing the
notion of induction on length l <= n, and destructing l and then rev l
with eqn:Heqe.