proposition: Lemma istrans_reverse {X : UU} (l : hrel X) : istrans l → istrans (hrel_reverse l).
proof: Proof. intros Hl x y z Hxy Hyz. now apply (Hl z y x). Qed.
imports: UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Sets