问Coq中单件类型单元的归纳原理是如何工作的？

EN

我正在阅读Adam Chlipala关于Coq的书，它定义了归纳类型：

Inductive unit : Set :=
  | tt.

我试着理解它的归纳原理：

Check unit_ind.
(* unit_ind
     : forall P : unit -> Prop, P tt -> forall u : unit, P u *)

我不确定是否理解了Coq的输出是什么意思。

1)所以check让我看一看“对象”的类型，对吗？所以unit_ind有以下类型：

forall P : unit -> Prop, P tt -> forall u : unit, P u

对吗？

2)如何读取该类型？我很难理解在逗号之前应该把括号或something...For放在哪里，这对我来说是没有意义的：

IF "for all P of type unit" THEN " Prop "

因为假设并不是真的或假的。所以我假设真正实现的第一件事是这样：

forall P : (unit -> Prop), ...

所以P只是类型unit to prop的函数。这是正确的吗？

我希望这是正确的，但在这种解释下，我不知道如何阅读第一个逗号后面的部分：

P tt -> forall u : unit, P u

我希望在命题一开始就定义现有变量的所有量化，但这不是它是如何完成的，所以我不确定发生了什么……

有人能帮我从形式上和直观上阅读这个命题吗？我还想从概念上理解它试图表达的意思，而不仅仅是被它的细节所困扰。