proposition: Lemma nfa_for_incl_correct X Y n (v : seq (vec n)): reflect (vec_lang (Incl X Y) v) (v \in nfa_lang (nfa_for_incl n X Y)).
proof: Proof. rewrite /nfa_lang inE. apply: (equivP existsP). rewrite (_ : (exists _,_) <-> nfa_accept (tt : nfa_for_incl n X Y) v); last first. - split => [[x]|];[case: x|exists tt]; by rewrite inE. - rewrite (_ : vec_lang _ _ <-> (forall u, u \in v -> nth false u X -> nth false u Y)). + elim: v => //= v vs IH. split. * case/exists_inP => [[/implyP A] /IH B] u /predU1P []; first by move=>?;subst. exact: B. * move => A. apply/exists_inP; exists tt;[apply/implyP|]. -- apply: A; exact: mem_head. -- apply/IH => u Hu. apply: A. by rewrite inE Hu orbT. + rewrite /vec_lang /=. split. * move => A u in_v u_X. set i := index u v. move: (A i). rewrite /I_of !mem_filter !mem_iota !add0n /=. rewrite index_mem in_v !andbT. rewrite nth_index //. by apply. * move => A => k. rewrite /I_of !mem_filter !mem_iota !add0n /=. case: (boolP (_ < _)); rewrite ?andbT ?andbF // => B. set u := nth [tuple of nseq n false] v k. apply A. by rewrite mem_nth. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)