Lemma isapropisStrongOrder {X : hSet} (R : hrel X) : isaprop (isStrongOrder R). Proof. apply isapropdirprod. - apply isaprop_istrans. - apply isapropdirprod. + apply isaprop_iscotrans. + apply isaprop_isirrefl. Defined.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.