proposition: Lemma prj_glue bs n (v : seq (vec n)) : exists k, prj0 (glue bs v) = v ++ nseq k [tuple of nseq n false].
proof: Proof. exists (size bs - size v). elim: bs v => [|b bs IH] v /=. - rewrite /prj0 -map_comp cats0 map_id_in //= => b. by rewrite !tupleE behead_cons. - case: v => [| v vs] /=; by rewrite IH /= ?subn0 ?subss !tupleE behead_cons. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)