proposition: Lemma nth_glue0 b n (v : seq (vec n)) k : nth false (nth [tuple of nseq n.+1 false] (glue b v) k) 0 = nth false b k.
proof: Proof. elim: k v b => [|k IH] [|v vs] [|b bs] //=. case: (ltnP k (size vs)) => A. - by rewrite (nth_map [tuple of nseq n false]) //. - by rewrite [_ _ _ k]nth_default // size_map. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)