Definition negforall_to_existsneg_restricted (H_LEM : LEM) {X:UU} {A B : hsubtype X} : ¬ (∀ x, A x ⇒ B x) ⇒ ∃ x, A x ∧ ¬ B x. Proof. intros H_forall. apply (proof_by_contradiction H_LEM). intros H_nex. use H_forall. intros x A_x. apply (proof_by_contradiction H_LEM). use (negexists_to_forallneg_restricted H_nex); assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo. Require Import UniMath.OrderTheory.Posets.Subposets.