(P : QuotientGroup -> Type) `{forall x, IsHProp (P x)} (H1 : forall x, P (grp_quotient_map x)) : forall x, P x. Proof. srapply Quotient_ind_hprop. exact H1. Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Congruence. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import HSet. Require Import Spaces.Finite.Finite. Require Import WildCat. Require Import Modalities.Modality.