我是Coq的新手，正在这里查看Mike Nahas的教程：nahas_tutorial.v。具体来说，我在理解下面给出的语句时遇到了麻烦：
Theorem forall_exists : (forall P : Set -> Prop, (forall x, ~(P x)) -> ~(exists x, P x)).
到目前为止是我的解释，欢迎更正。
Set -> Prop语句是一个命题，可以扩展为forall s: Set, Prop，我理解为“对于Set的每个证明（读实例），我们也都有Prop的证明（实例）” 。
因此，forall P : Set -> Prop可以粗略地理解为“对于集合引起命题的每个证明”。
然后是(forall x, ~(P x))，我猜测是Coq将x推定为Set类型，并被解读为“每个集合都产生了无法证明/错误的主张”。
并且对于~(exists x, P x)，我读到，因为没有集合暗示在P下存在一个真实的命题。
这些在逻辑上似乎是等效的。我只是在用语言挣扎。 P可以解释为从集合空间映射到命题空间的函数吗？我曾经用过“给……带来”和“暗示……存在”这两个词。它是否正确？有没有更正确的方式说明这一点？
感谢您提供所有帮助！
编辑：对于任何有类似问题的人，我的困惑大多等于对Curry-Howard同构一无所知。
Set -> Prop属于Type，不属于Prop。在Type中时，应将X -> Y视为从X到Y的函数，而在Prop中时，应将其读取为X表示Y（尽管库里·霍华德讲的是一样的。
[当函数返回Prop时，通常将其视为谓词或属性。因此，forall P : Set -> Prop可以理解为“对于每个Set值的属性...”