Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove

Theorem eta : forall (A : Type) (f : A -> A), (fun x => f x) = f?

Does this require functional extensionality?

Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove

Theorem eta : forall (A : Type) (f : A -> A), (fun x => f x) = f?

Does this require functional extensionality?

Edit: I already accepted an answer, but a better (followup) question would be, if Coq supports eta-conversion, why does Eval compute in (fun x => f x). not reduce to f?

Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove

Theorem eta : forall (A : Type) (f : A -> A), (fun x => f x)?

Does this require functional extensionality?

Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove

Theorem eta : forall (A : Type) (f : A -> A), (fun x => f x) = f?

Does this require functional extensionality?