proposition: Lemma starting_segment_exists_unique x (Cx: cond x): exists! l, << SORTED: StronglySorted r l >> /\ << INIT: forall x', cond x' /\ r^* x' x <-> In x' l >>.
proof: Proof. assert (X:=starting_segment_exists Cx); desc. destruct STO. exists l; split; ins; desc. eapply StronglySorted_eq; eauto. by ins; rewrite <- INIT, INIT0. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted