proposition: Lemma delta_bounded: forall A, eNFA.bounded A -> forall i a n x, StateLabelMap.MapsTo (i, a) x (eNFA.deltamap A) -> StateSet.In n x -> below n (eNFA.size A).
proof: Proof. intros [size eps delta initial final max_label] Hb i a n x Hx Hnx. simpl. apply (@eNFA.bounded_delta _ Hb a i). unfold eNFA.delta in *. simpl in *. apply StateLabelMapProps.find_mapsto_iff in Hx. rewrite Hx. apply Hnx. 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(Utils_WF) Coq(Relations) Coq(Eqdep_dec)