(a b : A) : class_of R a = class_of R b -> R a b. Proof. intros p. change (in_class (class_of R a) b). destruct p^. cbv; reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.