The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hello,

You can prove that the length are the same.
Arithmetic reasoning will do the rest.

Best,
—
Frédéric


> On 10 févr. 2015, at 13:31, Saulo Araujo 
> <saulo2 AT gmail.com>
>  wrote:
> 
> Hi,
> 
> I am trying to prove a theorem and got stuck. I have the following 
> hypothesis
> 
> H0 : l = (c, p) :: l
> 
> which says that a list is equal to the tail of another list. This, I 
> believe, is never true. Prooving another simpler theorem I also got in a 
> situation like this and, in that simpler case, I could end the proof using 
> the discriminate tactic, but in this case, Coq says:
> 
> Error: No primitive equality found.
> 
> Does anyone know what can I do?
> 
> Thanks in advance,
> Saulo