proposition: Lemma extract_word_tool : forall l, match extract_word l with | None => all delta2 l | Some u => exists e,exists f, (e,f,u) \in l /\ (predC delta2) (e,f,u) end.
proof: Proof. elim => [ | [[a b] u] tl hi] //=. case heq : (has_eps a == has_eps b) => //=. - move : hi. case: (extract_word tl) => //=. move => w [e [f [h1 h2]]]. exists e; exists f; rewrite in_cons. by rewrite h1 orbT. - by exists a; exists b; rewrite in_cons heq eq_refl. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)