proposition: Lemma path_in_class_of : forall q x, in_class q x -> q = class_of R x.
proof: Proof. srapply Quotient_ind. { intros x y p. apply (qglue p). } intros x y p. funext ? ?. apply hset_path2. Defined.
imports: Basics Types HSet TruncType Colimits.GraphQuotient Truncations.Core PropResizing