proposition: Lemma Book_3_14_equiv A : merely A <~> ~~A.
proof: Proof. apply equiv_iff_hprop. - apply Trunc_rec. exact (fun a na => na a). - intro nna. apply (@Book_3_14 A (fun _ => merely A)). * exact tr. * intros x y z w. apply path_ishprop. * exact nna. 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)