proposition: Lemma I_of_vecP k a w: k < size w -> (k \in I_of (vec_of w) (enum_rank a) = (nth a w k == a)).
proof: Proof. move => H. rewrite /vec_of /I_of mem_filter mem_iota add0n size_map /=. rewrite (nth_map a) // H andbT. rewrite (nth_map (enum_rank a)) ?size_tuple ?ltn_ord //. by rewrite nth_ord_enum (inj_eq enum_rank_inj) eq_sym. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)