proposition: Lemma I_of_glue0 i b n (v : seq (vec n)) : i \in I_of (glue b v) 0 = nth false b i.
proof: Proof. rewrite mem_filter mem_iota add0n leq0n andTb. rewrite nth_glue0 size_glue leq_max andbC. case: (ltnP i (size b)) => //= A. by rewrite nth_default ?andbF. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)