Lemma StrongOrder_reverse_correct {X : UU} (l : StrongOrder X) : ∏ x y : X, StrongOrder_reverse l x y = l y x. Proof. intros x y. now apply paths_refl. Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.