proposition: Lemma lex_istotal (X:hSet) (Y:X->hSet) (R:hrel X) (S : ∏ x, hrel (Y x)) : isdeceq X -> istotal R -> (∏ x, istotal(S x)) -> istotal (lexicographicOrder X Y R S).
proof: Proof. intros Xdec Rtot Stot u u'. induction u as [x y]. induction u' as [x' y']. induction (Xdec x x') as [eq|ne]. { refine (Stot x' (transportf Y eq y) y' _ _); intro P. induction P as [P|P]. { apply hdisj_in1. unfold lexicographicOrder; simpl. apply hdisj_in2. exact (eq,,P). } { apply hdisj_in2. unfold lexicographicOrder; simpl. apply hdisj_in2. induction eq. exact (idpath _,,P). } } { refine (Rtot x x' _ _); intro P. induction P as [P|P]. { apply hdisj_in1. apply hdisj_in1. simpl. exact (ne,,P). } { apply hdisj_in2. apply hdisj_in1. simpl. exact (ne ∘ pathsinv0,,P). } } Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions