相关疑难解决方法(0)

我正在阅读Mike Nahas的Coq教程,该教程说:

"ex_intro"的参数是:

• 谓词
• 证人
• 与证人一起打电话的证明

我查看了定义:

Inductive ex (A:Type) (P:A -> Prop) : Prop :=
  ex_intro : forall x:A, P x -> ex (A:=A) P.

而我在解析它时遇到了麻烦.表达式的哪些部分forall x:A, P x -> ex (A:=A) P对应于这三个参数(谓词,见证和证明)？

我定义了一个 Sygma-Type，它看起来像：

{ R : nat -> nat -> bool | Reflexive R }

我有两个要素r1 r2 : { R : nat -> nat -> bool | Reflexive R }，我要证明r1 = r2。我怎样才能做到这一点？