proposition: Lemma starting_segment_property x (Cx: cond x) : << SORTED: StronglySorted r (starting_segment Cx) >> /\ << INIT: forall x', cond x' /\ r^* x' x <-> In x' (starting_segment Cx) >>.
proof: Proof. unfold starting_segment; match goal with [ |- context[proj1_sig ?t] ] => destruct t end; eauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted