proposition: Lemma vec_Ex_prj0 s n (w : word (vec n.+1)) : vec_lang s w -> vec_lang (Ex s) (prj0 w).
proof: Proof. rewrite /vec_lang => /= A. exists [seq i <- iota 0 (size w) | nth false (nth [tuple of nseq n.+1 false] w i) 0]. apply: weak_coincidence A => X i. rewrite mem_filter mem_iota add0n /= /cons. case: X => [|X]. + by rewrite mem_filter mem_iota /= add0n. + rewrite mem_filter mem_iota add0n size_map /prj0 andTb -nth_behead. (case: (boolP (i < _)); rewrite ?andbF ?andbT //) => A. congr nth. by erewrite nth_map. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)