proposition: Lemma naive_LEM_implies_AC : (forall A : Type, A + ~A) -> forall X A P, (forall x : X, ~~{ a : A x | P x a }) -> { g : forall x, A x | forall x, P x (g x) }.
proof: Proof. intros LEM X A P H. pose (fun x => @naive_LEM_impl_DN_elim _ (LEM _) (H x)) as H'. exists (fun x => (H' x).1). exact (fun x => (H' x).2). Defined.
imports: HoTT(Basics Types HProp HSet Projective TruncType Truncations Modalities.Notnot Modalities.Open Modalities.Closed BoundedSearch Equiv.BiInv Spaces.Nat Spaces.Torus.TorusEquivCircles Metatheory.Core Metatheory.FunextVarieties)