proposition: Lemma preim_regular (char char' : finType) (h : word char -> word char') L : homomorphism h -> regular L -> regular (preimage h L).
proof: Proof. move => hom_h [A HA]. exists (dfa_preim h A) => w. by rewrite dfa_preimP // unfold_in /= -HA. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)