proposition: Lemma dfa_equiv_correct A1 A2 : reflect (dfa_lang A1 =i dfa_lang A2) (dfa_equiv A1 A2).
proof: Proof. apply: (iffP (dfa_emptyP _)) => H w. - move/negbT: (H w). rewrite !dfa_op_correct -addNb. move/addbP. by rewrite negbK. - apply/negbTE. by rewrite !dfa_op_correct H addbb. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)