proposition: Lemma nfa_for_ex_correct n s (A : nfa (vec n.+1)) v: (forall u, reflect (vec_lang s u) (u \in nfa_lang A)) -> reflect (vec_lang (Ex s) v) (v \in nfa_lang (nfa_for_ex A)).
proof: Proof. move => IHs. apply: (iffP idP). + case/nfa_for_exE => b. move/IHs. move/vec_Ex_prj0. case: (prj_glue b v) => k ->. by rewrite -vec_lang0. + case/vec_ex_glue => b. move/IHs. exact: nfa_for_exI. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)