proposition: Lemma dfa_emptyP : reflect (dfa_lang A =i pred0) (dfa_empty).
proof: Proof. apply: (iffP idP) => [/dec_eq H x|H]; first by rewrite inE /dfa_accept (negbTE (H _)). apply/dec_eq => x. by rewrite -[_ \notin _]/(x \notin dfa_lang A) H. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)