proposition: Lemma in_wder_compat : forall (r1 r2:bregexp), r1 ≡ r2 -> forall s, (wder s r1) ≡ (wder s r2).
proof: Proof. move => r1 r2 heq. elim/last_ind => [ | s a hi] //= u. rewrite -!cats1 !wder_cat /=. by apply in_der_compat. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)