proposition: Lemma start_of_starting_segment x (Cx : cond x) y (Cy : cond y) l l': starting_segment Cx = l ++ y :: l' -> starting_segment Cy = l ++ y :: nil.
proof: Proof. assert (T := STO); do 2 (red in T; desc). ins; eapply StronglySorted_eq; vauto. * by apply starting_segment_property. * eapply StronglySorted_app_l. rewrite <- app_assoc; ins. rewrite <- H. by apply starting_segment_property. * split; ins. + apply starting_segment_property in H0; desc. specialize (starting_segment_property Cx); ins; desf; rewrite H in *. forward apply (proj1 (INIT x0)) as X. { split; ins. eapply rt_trans; eauto. eapply starting_segment_property. rewrite H; eauto with hahn. } rewrite in_app_iff in X; ins; desf; eauto with hahn. exfalso. apply StronglySorted_app_r, StronglySorted_inv in SORTED; desf. rewrite Forall_forall in SORTED0. apply SORTED0 in X. rewrite clos_refl_transE in H1; desf. eby eapply T. apply (ct_of_trans T1) in H1. eby eapply T, T1. + apply starting_segment_property. specialize (starting_segment_property Cx); ins; desf; rewrite H in *. forward apply (proj2 (INIT x0)) as X. by rewrite in_app_iff in H0; ins; desf; eauto with hahn. split; desf. clear - H0 SORTED. rewrite in_app_iff in *; ins; desf; vauto. apply StronglySorted_app_iff in SORTED; desf. apply rt_step; eauto with hahn. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted