fact: Fixpoint re_image (e : regexp char) : regexp char' := match e with | Void => Void | Eps => Eps | Atom a => String (h [:: a]) | Star e => Star (re_image e) | Plus e1 e2 => Plus (re_image e1) (re_image e2) | Conc e1 e2 => Conc (re_image e1) (re_image e2) end.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)