proposition: Lemma dfa_op_correct w : w \in dfa_lang dfa_op = op (w \in dfa_lang A1) (w \in dfa_lang A2).
proof: Proof. rewrite !inE {2}/dfa_op /=. elim: w (dfa_s A1) (dfa_s A2) => [| a w IHw] x y; by rewrite !accE ?inE /=. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)