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