proposition: Lemma mem_I_of n (v : seq (vec n)) X k : (k \in I_of v X) = (k < size v) && nth false (nth [tuple of nseq n false] v k) X.
proof: Proof. by rewrite mem_filter mem_iota add0n /= andbC. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)