proposition: Lemma vec_lang0 s n (v : seq (vec n)) k : vec_lang s v <-> vec_lang s (v ++ nseq k [tuple of nseq n false]).
proof: Proof. apply coincidence => X ? i. rewrite !mem_filter !mem_iota /= !add0n size_cat nth_cat. case: (boolP (i < size v)) => Hi; first by rewrite ltn_addr. by rewrite andbF !(nth_nseq,if_same). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)