Lemma isrefl_reverse {X : UU} (l : hrel X) : isrefl l → isrefl (hrel_reverse l). Proof. intros Hl x. now apply Hl. Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.