proposition: Lemma nfa_for_exI n (A : nfa (vec n.+1)) b w : glue b w \in nfa_lang A -> w \in nfa_lang (nfa_for_ex A).
proof: Proof. rewrite /nfa_lang !inE. case/exists_inP => s s1 s2. apply/exists_inP. exists s => //. elim: b w s {s1} s2 => [w p /=|b bs IH w p]. - elim: w p => /= [|v w IHw] p. + rewrite /= inE => H. by apply/exists_inP; exists p. + apply: sub_exists => q /andP [q1 q2]. rewrite IHw // andbT. by apply/existsP;exists false. - case: w => [|v w] /=. + case/exists_inP => q q1 /IH /= q2. rewrite !inE in q2 *. apply: sub_exists q2 => r /andP [r1 r2]. rewrite r1 (connect_trans (connect1 _) r2) // /trans_b0. by apply/existsP;exists b. + apply: sub_exists => q /andP [q1 q2]. rewrite IH // andbT. by apply/existsP;exists b. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)