proposition: Lemma nfa_acceptP x p : reflect (exists r, nfa_run x p r) (nfa_accept p x).
proof: Proof. apply: (iffP idP) => [|[r]]. - elim: x p => [|a x IHx] p /=; first by exists [::]; constructor. case/exists_inP => q p1 p2. case (IHx q p2) => r ?. by exists (q::r); constructor. - elim: x r p => [|a x IHx] r p; first by inversion 1; subst. inversion 1; subst. apply/exists_inP. exists q => //. exact: IHx H4. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)