{A : Type@{i}} (R : Relation@{i j} A) (P : A / R -> Type) `{forall x, IsHProp (P x)} (dclass : forall a, P (class_of R a)) : forall x, P x. Proof. srapply (Quotient_ind R P dclass). intros x y p; apply path_ishprop. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.