proposition: Lemma max_common_initial_is_max {X:hSet} (S T : TOSubset X) (A : hsubtype X) : common_initial A S T -> A ⊆ max_common_initial S T.
proof: Proof. intros c x Ax. exact (hinhpr (A,,Ax,,c)). Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets