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.