The Coq mailing list

["fengsheng" <fsheng1990 AT 163.com>]

Hello everyone:
  I met a question of palindrome,the following is my definition of palindrome:
  Inductive pal {X : Type} : (list X) -> Prop :=
  | pal_empty :  pal []
  | pal_single : forall (x : X), pal [x]
  | pal_app: forall (x : X) (l: list X), pal l -> pal (x::(snoc l x)).

  Now, I want to prove:
  THeorem forall l, l = rev l -> pal l.
  But I counld not work it out.
  Counld you give me a proof of the theorem?