proposition: Lemma start_of_starting_endpoint x (Cx: cond x) : exists l, starting_segment Cx = l ++ x :: nil.
proof: Proof. assert (X:=starting_segment_contains_endpoint Cx). apply in_split in X; desf. enough (l2 = nil) by (desf; eauto). assert (Y:=starting_segment_property Cx); desf. rewrite X in *; clear X. apply StronglySorted_app_iff, proj2, proj1 in SORTED. apply StronglySorted_cons_iff, proj2 in SORTED. destruct l2; ins. rewrite Forall_cons in *. assert (r^* a x) by (apply INIT; eauto with hahn). destruct STO as [[IRR T] TOT]. exfalso; eapply IRR, ct_of_trans, t_rt_step; desf; vauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted