Why can't I destruct or discriminate here?

Question

I am proving the following theorem.

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

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  intros.
  unfold excluded_middle in H.
  unfold not in H0.
  unfold not in H.
  assert (P x \/ ~ P x).
  apply H.
  destruct H1.
  - apply H1.
  - unfold not in H1. 

Currently, the goal is

1 goal
H : forall P : Prop, P \/ (P -> False)
X : Type
P : X -> Prop
H0 : (exists x : X, P x -> False) -> False
x : X
H1 : P x -> False
______________________________________(1/1)
P x

If I have a goal like H -> False, I have something that has False in my hypothesis, I tend to use discriminate or destruct. However, now I have H -> False in my hypothesis, and H in my goal. I wonder why I can't use discriminate or destruct any more?

BTW, I know I can use exfalso in this case. However, IMO exfalso also intros the H, and then destruct H. So Is there any way to do this with destruct or destruct, and without assert.

Answer 1

destruct H0 does the same as exfalso; apply H0 (in a more primitive way).