proposition: Lemma Book_7_1_part_i (H : forall A, merely A -> A) A : IsHSet A.
proof: Proof. apply (@HoTT.HSet.ishset_hrel_subpaths A (fun x y => merely (x = y))); try typeclasses eauto. - intros ?. apply tr. reflexivity. - intros. apply H. assumption. 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)