proposition: Lemma build_list_der_ok : forall (E:bregexp) u, exists F:bregexp, exists v, ((F,v) \in (build_list_der E)) /\ (wder u E) ≡ F.
proof: Proof. move => E u. set L := build_list_fun E E. case: (@tool_bl L _ E E _ u) => [ | | f [f' [v [h1 h2 h3]]]]. - rewrite /L /build_list_fun. apply: l3. by apply: lminus_incl. - apply: (linclP [:: (E,E,[::])]). by apply: l1. by rewrite /= in_cons eq_refl. exists f; exists v; split => //. rewrite /build_list_der. move/strip_in : h1. rewrite /L => h; exact h. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)