我遇到了一个问题，我不知道这是否是伊莎贝尔管理集合理解的方式，或者我遇到了一个非常缓慢的时刻。
这个引理继续得很好
lemma "{x | x. P x} ∩ {x | x y. (Q x y)} = {x | x y. (P x) ∧ (Q x y)}"
by auto
而这个却没有
lemma "{x | x y. (P x y)} ∩ {x | x y z. (Q x y z)} = {x | x y z. (P x y) ∧ (Q x y z)}"
两者之间一定有区别，但我看不出来。显然，我需要第二个，我的(P x y)和(Q x y z)非常复杂，我很难简化它。
像往常一样，我们非常感谢任何帮助（或将我引导到一些更健康的方向）。
左侧
{x | x y. P x y} ∩ {x | x y z. Q x y z}包含所有x包含该内容的内容(∃y. P x y) ∧ (∃y z. Q x y z)。右侧
{x | x y z. P x y ∧ Q x y z}包含所有x包含该内容的内容∃y z. P x y ∧ Q x y z。不同之处在于，前一个限制较弱，因为“
y使P x y发生”和“y使Q x y z发生”不必相同。情况
{x | x. P x} ∩ {x | x y. (Q x y)} = {x | x y. (P x) ∧ (Q x y)}有所不同，因为唯一的共享变量是x，但x有点特殊。如果将上述陈述简化为量词，可能会更清楚一点：第一个基本上是说，对于所有
x：而第二个则说，对于所有人来说
X：