The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

Hello,
do you think this can be proved in Coq under some conditions or can it be 
safely assumed as an axiom?

Conjecture type_extensionality :  forall A (T1: A -> Type) (T2: A -> Type),
    (forall a, T1 a = T2 a) -> (forall a, T1 a) = (forall a, T2 a).

Thanks for any idea,
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France