proposition: Lemma palindrome_rev : forall l:list A, palindrome l -> rev l = l.
proof: Proof. intros l H; elim H; simpl; auto with datatypes. intros a l0 m H0 H1 H2; generalize H1; inversion_clear H2. - simpl; auto. - rewrite (remove_last_inv _ _ _ H3); simpl; repeat (rewrite rev_app; simpl). intro eg; rewrite eg; simpl; auto. Qed.
imports: List Arith Lia