proposition: Lemma classes_eq_related : forall x y, class_of R x = class_of R y -> R x y.
proof: 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.
imports: HoTT.Basics HoTT.Types HSet TruncType Truncations.Core