forall x a, in_class x a -> x = class_of R a. Proof. srapply Quotient_ind. { intros a b p. exact (qglue p). } intros a b p. funext ? ?. apply hset_path2. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.