proposition: Lemma dfa_incl_correct A1 A2 : reflect {subset dfa_lang A1 <= dfa_lang A2} (dfa_incl A1 A2).
proof: Proof. apply: (iffP (dfa_emptyP _)) => H w. - move/negbT: (H w). rewrite dfa_op_correct -negb_imply negbK. by move/implyP. - rewrite dfa_op_correct -negb_imply. apply/negbTE. rewrite negbK. apply/implyP. exact: H. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)