proposition: Lemma X_to_DFA_bounded: forall a, DFA.bounded (X_to_DFA a).
proof: Proof. intro a. apply DKA_Determinisation.bounded, DKA_Epsilon.bounded, DKA_Construction.bounded. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Converse) ATBR(DKA_Definitions) Coq(List)