proposition: Lemma iscotrans_reverse {X : UU} (l : hrel X) : iscotrans l -> iscotrans (hrel_reverse l).
proof: Proof. intros Hl x y z H. now apply islogeqcommhdisj, Hl. Qed.
imports: UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Sets