coq - 如何在 Coq 中结束这个证明

Question

我已经设法将我的目标降低到

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

我知道 reflexivity会起作用，但出于教学原因，我更愿意继续减少它。
me是一个恒等函数，所以 unfold me将其简化为

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

这只是一个应用函数 x 的匿名函数到虚拟变量 x0 ，所以你可以说两边都只是函数 x .如果可能的话，我想在双方达成相同的表达。

Answer 1

你可以:

Require Import FunctionalExtensionality.

进而:

rewrite -> eta_expansion.

不过，这使用了依赖函数可扩展性的公理。