fact: Definition quotient_ind_prop' : forall P : quotient R -> Type, forall (Hprop' : forall x, IsHProp (P (class_of _ x))), (forall x, P (class_of _ x)) -> forall y, P y.
imports: HoTT.Basics HoTT.Types HSet TruncType Truncations.Core