diff --git a/quantifiers_and_equality.md b/quantifiers_and_equality.md
index b6da4b4..07de2b7 100644
--- a/quantifiers_and_equality.md
+++ b/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``，就得到构建涉及全称量词的证明的规则。