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 を破棄する前に左または右のいずれも適用できないことです。

それを行う簡単な方法はありますか？