proposition: Lemma lift_accept p q x : q \in eps_reach p -> enfa_accept q x -> enfa_accept p x.
proof: Proof. rewrite inE => /connectP [s]. elim: s p x q => //= [p x q _ -> //| q s IHs p x q']. case/andP => pq ? ? H. apply: EnfaNone pq _. exact: IHs H. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)