如何在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.

但这使用了依赖函数外延性的公理。