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