fact: Definition StrongOrder_setquot {X : UU} {R : eqrel X} {L : StrongOrder X} (is : iscomprelrel R L) : StrongOrder (setquot R) := quotrel is,, isStrongOrder_setquot is (pr2 L).
imports: UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Sets