proposition: Lemma iseqrel_eqrel_from_hrel : iseqrel eqrel_from_hrel.
proof: Proof. repeat split. - intros x y z H1 H2 R HR. exact (eqreltrans _ _ _ _ (H1 _ HR) (H2 _ HR)). - now intros x R _; apply (eqrelrefl R). - intros x y H R H'. exact (eqrelsymm _ _ _ (H _ H')). Qed.
imports: UniMath.MoreFoundations.Propositions UniMath.Foundations.Sets