fact: Definition nfa_for_ex n (A : nfa (vec n.+1)) : nfa (vec n) := {| nfa_s := nfa_s A; nfa_fin := [set p | [exists (q | q \in nfa_fin A), connect (trans_b0 A) p q]]; nfa_trans := fun p (v : vec n) q => [exists b, nfa_trans p [tuple of b::v] q] |}.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)