proposition: Lemma NoDup_starting_segment x (Cx: cond x) : NoDup (starting_segment Cx).
proof: Proof. destruct STO as [[IRR T] TOT]. eapply NoDup_StronglySorted; eauto. apply starting_segment_property. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted