proposition: Lemma EQUIV3 : forall E F, E ≡ F <-> (forall e f, set_pair_der E F (e,f) -> has_eps e = has_eps f).
proof: Proof. rewrite /EQUIV => E F; split => h. - rewrite /set_pair_der. move => e f [s] h1 h2. rewrite (has_eps_sim h1) (has_eps_sim h2) -!mem_wder !mem_derE. by apply: h. - rewrite /set_pair_der in h => s. apply EQUIV2. move => t. rewrite (h (wder t E) (wder t F)) => //. exists t; reflexivity. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)