proposition: Lemma quotient_ind_prop (P : quotient R -> Type) `{forall x, IsHProp (P x)} : forall dclass : forall x, P (class_of R x), forall q, P q.
proof: Proof. intros. apply (quotient_ind R P dclass). intros. apply path_ishprop. Defined.
imports: HoTT.Basics HoTT.Types HSet TruncType Truncations.Core