我想证明以下定理
Goal (forall x, P x \/ Q x) -> (forall x, P x) \/ (forall x, Q x).
有上下文
1 subgoal
P : nat -> Prop
Q : nat -> Prop
R : nat -> nat -> Prop
H : forall x : nat, P x \/ Q x
______________________________________(1/1)
(forall x : nat, P x) \/ (forall x : nat, Q x)
该陈述在谓词逻辑中似乎是正确的,但我不知道如何证明它。问题本质上是我不能一次消除所有的 forall,但我不能在破坏假设 H 之前既不向左也不向右应用。
有没有一种简单的方法可以做到这一点?