proposition: Theorem well_founded: forall (a: regex), strict_star_form a -> eNFA.well_founded (X_to_eNFA a).
proof: Proof. intros a Ha. apply incl_wf with (transp _ (epsilon (build a 0 1 empty))). apply wf_build. exact Ha. apply bounded_empty. reflexivity. reflexivity. apply wf_empty. intro H. apply trans_rt1n in H. inversion_clear H. elim (epsilon_empty H0). intros i j Hij. unfold X_to_eNFA in Hij. destruct (build a 0 1 empty). apply Hij. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)