The Coq mailing list

[casteran AT labri.fr]

Selon june andronick 
<jandronick AT axalto.com>:
> ...

Hello, June,

 I forgot some contributions by Jean Duprat, Bruno Barras, and C.T. McBride,
about case analysis on vectors (you can find them by searching "vectors"
in the Club archive).

I attach to this mail a full version, including Jean Duprat's and
Laurent Thery's proofs. It can be improved, but it works :-)



Pierre



> Hello,

> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

Attachment: vectors.v
Description: Binary data