proposition: Lemma im_regular (char char' : finType) (h : word char -> word char') L : homomorphism h -> regular L -> regular (image h L).
proof: Proof. move => hom_h /regularP [e He]. apply/regularP. exists (@re_image _ _ h e) => w. transitivity (image h (re_lang e) w); first exact: image_ext. exact: rwP (re_imageP _ _ _). Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)