forall x y, class_of R x = class_of R y -> R x y. Proof. intros x y H'. pattern (R x y). eapply transport. - apply in_class_pr. - pattern (class_of R x). apply (transport _ (H'^)). apply Hrefl. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.