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