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