Definition lexicographicOrder (X:hSet) (Y:X->hSet) (R:hrel X) (S : ∏ x, hrel (Y x)) : hrel (∑ x, Y x)%set.
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.