proposition: Theorem rev_pal : forall l:list A, rev l = l -> palindrome l.
proof: Proof. intro l; elim l using list_new_ind; auto. - intros a b l0 H H0. apply cons_pal with l0. + apply H; simpl in H0; rewrite rev_app in H0. simpl in H0; injection H0. intros H1 e; generalize H1; rewrite e. intro H2; generalize (app_right_reg _ _ _ H2); auto. + simpl in H0; rewrite rev_app in H0; simpl in H0. injection H0; intros H1 H2; rewrite <- H2. generalize l0; intro l1; induction l1; simpl; auto. Qed.
imports: List Arith Lia