proposition: Lemma Inter_correct (char : finType) (r s : regexp char) w : w \in Inter r s = (w \in r) && (w \in s).
proof: Proof. by rewrite /Inter -dfa_to_re_correct dfa_op_correct !re_to_dfa_correct. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)