proposition: Lemma re_to_dfa_correct (r : regexp char) : dfa_lang (re_to_dfa r) =i r.
proof: Proof. move => w. by rewrite -nfa_to_dfa_correct re_to_nfa_correct. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)