proposition: Lemma iseqrel_reverse {X : UU} (l : hrel X) : iseqrel l → iseqrel (hrel_reverse l).
proof: Proof. intros H. split. now apply ispreorder_reverse, (pr1 H). now apply issymm_reverse, (pr2 H). Qed.
imports: UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Sets