proposition: Lemma EQUIV2 : forall E F, E ≡ F <-> forall s, (has_eps (wder s E)) = (has_eps (wder s F)).
proof: Proof. rewrite /EQUIV => E F. split => h. - move => s. rewrite -2!mem_wder 2!mem_derE. by apply: h. - move => s. rewrite -2!mem_derE 2!mem_wder. by apply: h. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)