proposition: Lemma re_equiv_correct r s : reflect (r =i s) (re_equiv r s).
proof: Proof. apply: (iffP (dfa_equiv_correct _ _)) => H w; move/(_ w) : H; by rewrite !re_to_dfa_correct. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)