proposition: Lemma class_of_repr : forall q x, in_class q x -> q = class_of R x.
proof: Proof. apply (quotient_ind R (fun q : quotient R => forall x, in_class q x -> q = class_of _ x) (fun x y H => related_classes_eq R H)). intros. apply path_forall. intro z. apply path_forall;intro H'. apply quotient_path2. Defined.
imports: HoTT.Basics HoTT.Types HSet TruncType Truncations.Core