proposition: Lemma mem_R0 w x y : reflect (w = [::] /\ x=y \/ exists2 a, w = [::a] & dfa_trans x a = y) (w \in R0 x y).
proof: Proof. apply: (iffP plusP). - case => [| /edgesP]; auto. case e : (x == y) => // /eqP. by rewrite (eqP e); auto. - case => [[-> ->]|/edgesP];auto. by rewrite eqxx; auto. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)