proposition: Theorem nfa_of_form_correct n (v : seq (n.-tuple bool)) s : reflect (vec_lang s v) (v \in nfa_lang (nfa_of_form n s)).
proof: Proof. elim: s n v => [X Y|X Y||s IHs t IHt|s IHs] /= n v. - exact: nfa_for_incl_correct. - exact: nfa_for_ltn_correct. - rewrite -dfa_to_nfa_correct in_simpl (negbTE (dfa_void_correct _ _)). by constructor. - rewrite -dfa_to_nfa_correct dfa_op_correct -!nfa_to_dfa_correct. by apply: (iffP implyP) => A /IHs/A/IHt. - exact: nfa_for_ex_correct. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)