fact: Definition naive_LEM_impl_DN_elim (A : Type) (LEM : A + ~A) : ~~A -> A := fun nna => match LEM with | inl a => a | inr na => match nna na with end end.
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)