proposition: Lemma isincl_underlyingPoset : isincl underlyingPoset.
proof: Proof. apply isinclpr1. intros X. apply isaprop_istotal. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions