The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Hello,

Coq's reference manual mentions eta-conversion only briefly, c.f. chapter
4.3 of it. Is the

Theorem eta_conversion :
   forall (A:Type) (B:A->Type) (f:forall x:A,B x),
   (fun x:A=>f x) = f.

provable in Coq without additional axioms?

A little bit more general is:

Theorem app_eq :
   forall (A:Type) (B:A->Type) (f g:forall x:A,B x),
   (forall x:A=>f x=g x) -> f = g.

If this is provable, then eta_conversion is easy to prove:

Lemma eta_conv :
   forall (A:Type) (B:A->Type) (f:forall x:A,B x),
   (fun x:A=>f x) = f.
Proof.
   intros A B f; apply app_eq.
   intro x; reflexivity.
Qed.

Regards,
-- 
Stefan Karrmann