proposition: Lemma vec_of_val_agrees : forall I n, agree n I (I_of (vec_of_val I n)).
proof: Proof. move => I n X lt_n i. rewrite mem_filter mem_iota /= add0n size_map size_iota. case: (boolP (i < _)); rewrite ?(andbT,andbF) => A. + rewrite /vec_of_val. rewrite (nth_map 0) ?size_iota // nth_iota // add0n. by rewrite (nth_map (Ordinal lt_n)) ?size_enum_ord ?nth_enum_ord. + apply: contraNF A => A. rewrite ltnS. rewrite /lim. apply: bigmax_sup => //. instantiate (1 := Ordinal lt_n) => /=. exact: bigmax_sup_seq A _ _ . Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)