Hello,

Please see attached file and code.

My question is: why this “destruct” acts like this? what is happening? we have disjunctive pattern with 0 branches here… but destruct works… and changes goal… and leads us to the victory.

```
(* Exercise: 3 stars, advanced (not_exists_dist) *)
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 EM X P H x.
unfold not in H.
destruct (EM (P x)) as [H2 | H3].
apply H2.
destruct H.
exists x.
apply H3.
Qed.
```