proposition: Lemma I_of_glueS i b n (v : seq (vec n)) k : i \in I_of (glue b v) k.+1 = nth false (nth [tuple of nseq n false] v i) k.
proof: Proof. rewrite mem_filter mem_iota add0n leq0n andTb. rewrite nth_glueS size_glue leq_max andbC orbC. case: (ltnP i (size v)) => //= A. by rewrite [_ _ v i]nth_default // nth_nseq if_same andbF. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)