The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

> Inductive data type for palindrome.
> 
> Inductive pal { X : Type } : list X -> Prop :=
>  | emptyC : pal nil
>  | consC : forall ( a : X ) ( l : list X ) , pal l -> pal ( a :: l ++ [a]).
> 

With this definition you capture only palindromes with a length that is even
> 
> Theorem reverseonlist : forall { X : Type } ( l : list X ), pal ( l >
> ++ rev
> l).> Proof.
> intros X l. induction l as [ | v' l'].
>   simpl. apply emptyC.
> simpl.


With assert you can see that both term does not match there is an
associativity problem

Try

 rewrite app_assoc.


--
Laurent