The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT inria.fr>]

>  L'ajout de l'axiome suivant
> remettrait-il en cause la cohérence du système Coq ?
> 
>      Axiom extensionality_Stream : (A:Set)(x,y:(Stream A))(EqSt ? x
>      y)->x=y.

Je suis (presque) sur que non. Je ne me suis jamais mis a` faire la
preuve en detail, mais je crois que on peut tres facilement adapter
celle que Martin Hofmann a fait dans la section 6.2 de sa these:

@PHDTHESIS{MH95,
        AUTHOR          = {M. Hofmann},
        SCHOOL          = {University of Edinburgh},
        TITLE           = {Extensional Concepts in Intentional Type Theory},
        YEAR            = {1995},
        key             = {ECS-LFCS-95-327},
        month           = {July}
}

L'axiome ne gene pas a` l'extraction non plus, car tout se pase dans
l'univers des propositions.

Amicalement,
Eduardo.