proposition: Lemma related_quotient_paths : forall x y, class_of R x = class_of R y -> R x y.
proof: Proof. intros x y p. change (in_class (class_of R x) y). destruct p^. cbv; reflexivity. Defined.
imports: Basics Types HSet TruncType Colimits.GraphQuotient Truncations.Core PropResizing