Definition negexists_to_forallneg_restricted {X:UU} {A B : hsubtype X} : ¬ (∃ x, A x ∧ B x) ⇒ (∀ x, A x ⇒ ¬ B x). Proof. intros H_nex x A_x B_x. use H_nex. apply hinhpr. exists x. split; 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.