proposition: 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: Proof. intros Srefl u. induction u as [x y]. apply hdisj_in2; simpl. exists (idpath x). apply Srefl. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions