How to end this Proof in Coq

Question

I have 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 reducing it.

me is an identity function so unfold me simplifies it to

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

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

Answer 1

You can:

Require Import FunctionalExtensionality.

and then:

rewrite -> eta_expansion.

This uses the axiom of dependent functional extensionality though.