Definition StrongOrder_reverse {X : UU} (l : StrongOrder X) := make_StrongOrder (hrel_reverse l) (isStrongOrder_reverse l (pr2 l)).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.