proposition: Lemma regularP (char : finType) (L : lang char) : regular L <-T-> { e : regexp char | forall x, L x <-> x \in e}.
proof: Proof. split => [[A HA]|[e He]]. - exists (dfa_to_re A) => x. by rewrite -dfa_to_re_correct. - exists (re_to_dfa e) => x. by rewrite re_to_dfa_correct. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)