proposition: Lemma dfa_preimP A : dfa_lang (dfa_preim A) =i preim h (dfa_lang A).
proof: Proof. Proof using h_hom. move => w. rewrite !inE /dfa_accept /dfa_preim /=. elim: w (dfa_s A) => [|a w IHw] x /= ; first by rewrite h0. by rewrite -[a :: w]cat1s h_hom !delta_cat -IHw. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)