proposition: Lemma delta_rc x y a : let s := dfa_s A in delta s x = delta s y -> delta s (x ++ [::a]) = delta s (y ++ [::a]).
proof: Proof. by rewrite /= !delta_cat => <-. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)