predicate - Coq - 假设中的通用量词

Question

我想证明以下定理

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 之前既不向左也不向右应用。

有没有一种简单的方法可以做到这一点？

Answer 1

P认为是均匀的，是奇怪的，你Q应该看到你的定理是有缺陷的。