如何利用Coq中包含forall的假设?

我试图证明 P \/ Q 和 ~ P -> Q

Theorem eq_of_or :
  excluded_middle ->
  forall P Q : Prop,
    (P \/ Q) <-> (~ P -> Q).

其中排除的中间值如下。

Definition excluded_middle := forall P : Prop, P \/ ~ P.

实际上,一个方向的证明不需要排除中间。在我试图证明另一个方向时,当我试图利用假设中被排除的中间点时,我陷入了困境,

Proof.
  intros EM P Q. split.
  { intros [H | H]. intros HNP. 
    - unfold not in HNP. exfalso.
      apply HNP. apply H.
    - intros HNP. apply H. }
  { intros H. unfold excluded_middle in EM.
    unfold not in EM. unfold not in H.
  }

其中,当前环境如下:

1 subgoal
EM : forall P : Prop, P \/ (P -> False)
P, Q : Prop
H : (P -> False) -> Q
______________________________________(1/1)
P \/ Q

left right ,如果我的证明到现在为止有意义的话。

提前感谢您的任何建议和建议!