The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2014-10-02 18:30 GMT+02:00 Cedric Auger 
<sedrikov AT gmail.com>:
> You got tricked with indice, Pierre. The correct form is the following one:


Ops indeed I was tricked.

To cover all the mathematical content from the sequence, you should
probably also prove a unicity result on the sequence: forall n x y, w
n x -> w n y -> x = y.

Best regards
P.