The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

David Leduc wrote:
> How can I prove the lemma cnuf below?
>
> Inductive eqfun : forall X Y, (X->Y) ->  (X->Y) ->  Prop :=
> | refl : forall X Y (f:X->Y), eqfun X Y f f
> | func : forall X Y Z (f g:X->Y->Z), (forall x, eqfun Y Z (f x) (g x))
> ->  eqfun X (Y->Z) f g.
>
> Lemma cnuf : forall X Y Z f g, eqfun X (Y->Z) f g ->  (forall x, eqfun
> Y Z (f x) (g x)).
>    

It's not obvious to me that your lemma is provable, even given the full 
set of axioms commonly assumed in Coq developments.  You must 
fundamentally do inversion on [eqfun] with a particular function type as 
a parameter, which seems to call for a proof step going from [(D1 -> R1) 
= (D2 -> R2)] to [D1 = D2] and [R1 = R2], but I don't think such a rule 
is provable in CIC, and I don't think any of the common axioms imply the 
soundness of this step.  It may be validated by the usual Boolean model 
in ZF, so perhaps it would be consistent to assert this as an axiom.

Or perhaps you could tell us more about the larger context of your 
development, and we could suggest ways to avoid depending on lemma [cnuf].