proposition: Lemma starting_segment_decomp x (Cx: cond x) y (Cy: cond y) (Rxy: r^* x y): starting_segment Cy = starting_segment Cx ++ segment Cx Cy.
proof: Proof. destruct STO as [[IRR T] TOT]. eapply StronglySorted_eq; eauto. * by red; eauto. * by apply starting_segment_property. * apply StronglySorted_app; ins. by apply starting_segment_property. by apply segment_property. apply starting_segment_property in IN1; apply segment_property in IN2; desf. rewrite clos_refl_transE in *; desf; eauto. all: repeat match goal with H : _⁺ _ _ |- _ => apply (ct_of_trans T) in H end; eauto. * ins; rewrite in_app_iff, !in_starting_segment_iff, in_segment_iff. intuition; eauto using clos_refl_trans. tertium_non_datur (x0 = x) as [->|NEQ]; eauto using clos_refl_trans. eapply TOT in NEQ; desf; eauto using clos_refl_trans. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted