The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> For what its worth, the reason I first considered this property above is
> because it appeared necessary in order to prove the following fact 
> concerning
> heterogeneous equalities:
> 
> Theorem JMeq_f :
>   forall A (B: A -> Type) (C: A -> Type) (f: forall a, B a) (g: forall a, C 
> a),
>     JMeq f g ->
>     forall x, JMeq (f x) (g x).

This reminds me of Nicolas Oury's embedding of the extensional
Calculus of Inductive Constructions into the intensional one [1,2]. As
far as I can recollect, he convinced himself at some point that your
theorem was not provable and took it as an axiom.

Best,

Hugo Herbelin

[1] N. Oury, Extensionality in the Calculus of Constructions, TPHOLs'05
[2] N. Oury, Égalité et filtrage avec types dépendants dans le Calcul
    des Constructions Inductives, PhD thesis, 2006.