proposition: Lemma Book_3_6_solution_1 `{Funext} (A : Type) : IsHProp A -> IsHProp (A + ~A).
proof: Proof. intro isHProp_A. apply hprop_allpath. intros x y. destruct x as [a1|n1]; destruct y as [a2|n2]; apply path_sum; try apply path_ishprop. - exact (n2 a1). - exact (n1 a2). 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)