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