proposition: Lemma vec_ex_glue s n (vs : seq (vec n)) : vec_lang (Ex s) vs -> exists bs, vec_lang s (glue bs vs).
proof: Proof. rewrite /vec_lang /= => [[N sat_s]]. exists [seq i \in N | i <- iota 0 (\max_(k <- N) k).+1]. apply: weak_coincidence sat_s => X i. case: X => [|X]. - rewrite I_of_glue0. case: (boolP (i < (\max_(k <- N) k).+1)) => ltn_max. + by rewrite (nth_map 0) ?size_iota // nth_iota. + rewrite nth_default ?size_map ?size_iota 1?leqNgt //. apply: contraNF ltn_max => H. rewrite ltnS. exact: bigmax_sup_seq H _ _. - rewrite I_of_glueS /= /I_of mem_filter mem_iota /= add0n. case: (ltnP i (size vs)) => H; first by rewrite andbT. rewrite andbF [nth _ _ i]nth_default //. by rewrite nth_nseq if_same. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)