The Coq mailing list

[Henri Fraisse <henri.fraisse AT trusted-logic.fr>]

Ca doit sans doute etre tres simple, mais je ne vois pas comment
montrer l'axiome d'extensionnalite pour les fonctions, a savoir:

Lemma ext:(A,B:Set)(f,g:A->B)((a:A)(f a)=(g a))->f=g.

(je ne l'ai pas non plus trouve en tant qu'axiome dans les bibliothèques et
je n'ai rien trouve a ce sujet dans le manuel).

quelqu'un peut-il me renseigner sur ce point la?

merci d'avance

-- 
=========================================================================

Henri Fraisse

+----------------------------------+------------------------------------+
| Henri FRAISSE                    |      TRUSTED LOGIC S.A.            |
| Henri.Fraisse AT trusted-logic.fr   |                                    |
| Phone: +33 01 30 97 25 04        |     5, rue du Bailliage,           |
| Secr.: +33 01 30 97 25 00        |       78000 Versailles             |
| Fax:   +33 01 30 97 25 19        |           FRANCE                   |
+----------------------------------+------------------------------------+