fact: Definition starting_segment x Cx := proj1_sig (constructive_definite_description _ (@starting_segment_exists_unique x Cx)).
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted