The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi Anton!

Anton Trunov 
<anton.a.trunov AT gmail.com>
 writes:

> Emilio, thank you for a nice exercise!
> The simplest solution I could come up with is like so:
>
> From Coq Require Import Vector.
> Fact rev_nil A : rev (nil A) = nil A.
> Proof.
>   generalize (rev (nil A)).
>   now apply case0.
> Qed.

Oh, that is very cool, indeed ! Thanks!

However this trick may not work so easily when you really have to use
the definition of rev:

Lemma rev_rev A n (v : t A n) : rev (rev v) = v.

;)

Cheers,
E.