润色 quantifiers_and_equality.md

将 

> Given a proof of p x, in a context where x : α is arbitrary, we obtain a proof ∀ x : α, p x.

的翻译改成了更符合汉语语序的方式，原来的翻译易造成误解：

错误理解：

> 给定 p x 的证明，** 在 x : α 是任意的情况下，我们得到 ∀ x : α, p x 的证明。**

正确理解：

> **给定 p x 的证明， 在 x : α 是任意的情况下**；我们得到 ∀ x : α, p x 的证明。

quantifiers_and_equality.md

@@ -76,19 +76,19 @@ Here is an example of how the propositions-as-types correspondence gets put into
 
 全称量词 ``∀ x : α, p x`` 表示，对于每一个 ``x : α``，``p x`` 成立。与命题连接词一样，在自然演绎系统中，「forall」有引入和消去规则。非正式地，引入规则是：
 
-> 给定 ``p x`` 的证明，在 ``x : α`` 是任意的情况下，我们得到 ``∀ x : α, p x`` 的证明。
+> 在 ``x : α`` 是任意的情况下，给定 ``p x`` 的证明；就可以得到 ``∀ x : α, p x`` 的证明。
 
 消去规则是：
 
-> 给定 ``∀ x : α, p x`` 的证明和任何项 ``t : α``，我们得到 ``p t`` 的证明。
+> 给定 ``∀ x : α, p x`` 的证明和任何项 ``t : α``，就可以得到 ``p t`` 的证明。
 
 与蕴含的情况一样，命题即类型。回想依值箭头类型的引入规则:
 
-> 给定类型为 ``β x`` 的项 ``t``，在 ``x : α`` 是任意的情况下，我们有 ``(fun x : α => t) : (x : α) → β x``。
+> 在 ``x : α`` 是任意的情况下给定类型为 ``β x`` 的项 ``t``，就可以得到 ``(fun x : α => t) : (x : α) → β x``。
 
 消去规则：
 
-> 给定项 ``s : (x : α) → β x`` 和任何项 ``t : α``，我们有 ``s t : β t``。
+> 给定项 ``s : (x : α) → β x`` 和任何项 ``t : α``，就可以得到 ``s t : β t``。
 
 在 ``p x`` 具有 ``Prop`` 类型的情况下，如果我们用 ``∀ x : α, p x`` 替换 ``(x : α) → β x``，就得到构建涉及全称量词的证明的规则。