forall q x, in_class q x -> q = class_of R x. 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.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.