proposition: Lemma dfa_quotP x : reflect (quotR x) (x \in dfa_lang dfa_quot).
proof: Proof. Proof using acc_L1. apply: (iffP idP). - rewrite inE /dfa_accept inE. case/dec_eq => y inL2. rewrite /dfa_accept -delta_cat => H. exists y => //. by rewrite -acc_L1. - case => y y1 y2. rewrite inE /dfa_accept inE /= dec_eq. exists y => //. by rewrite /dfa_accept -delta_cat acc_L1. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)