proposition: Lemma cat_prefix I n (Ns : n.-tuple (seq nat)) X : X < n -> cat Ns I X = nth [::] Ns X.
proof: Proof. move => A. by rewrite /cat size_tuple A. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)