Lemma lex_isrefl (X:hSet) (Y:X->hSet) (R:hrel X) (S : ∏ x, hrel (Y x)) : (∏ x, isrefl(S x)) -> isrefl (lexicographicOrder X Y R S). Proof. intros Srefl u. induction u as [x y]. apply hdisj_in2; simpl. exists (idpath x). apply Srefl. Defined.
Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.OrderTheory.Posets.Examples.StandardFiniteSet.