Lemma iseqrel_eqrel_from_hrel : iseqrel eqrel_from_hrel. 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.