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. intros c x Ax. exact (hinhpr (A,,Ax,,c)). Defined.
Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets.