proposition: Lemma dfa_L x y w : w \in L^setT x y = (delta x w == y).
proof: Proof. rewrite unfold_in. case: (_ == _) => //=. apply/forall_inP => ? ?. by rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)