How to end this proof in Coq

Question

I managed to reduce my goal to

(fun x0 : PSR => me (x x0)) = x 

I know that reflexivity will work, but for pedagogical reasons, I prefer to continue to reduce it.

me is an identical function, therefore unfold me simplifies it to

 (fun x0 : PSR => x x0) = x 

which is just an anonymous function that applies the function x to the dummy variable x0 , so you can say that both sides are just the function x . If possible, I would like to achieve the same expression on both sides.

Answer 1

You can:

 Require Import FunctionalExtensionality. 

and then:

 rewrite -> eta_expansion. 

In this case, the axiom of dependent functional extensibility is used.