proposition: Lemma tool_bl : forall (Y:seq (bregexp*bregexp*bword)), r_subset sim3 (DER Y) Y -> forall e e', ((e,e',[::]) \in Y) -> forall u, exists f, exists f', exists v, [/\ (f,f',v) \in Y , (wder u e) ≡ f & (wder u e') ≡ f'].
proof: Proof. move => Y hsub e e' he. elim/last_ind => [ | u a hi] /=. - by exists e; exists e'; exists [::]; split . - case: hi => f [f' [v [hf1 hf2 hf3]]]. move/(@R_elim _ _ sim3_Eq sim_dec3) : hsub. have hf : (InA sim_dec3 (DER Y) (der a f,der a f',a::v)). + case: a. by apply: In_DER1. by apply: In_DER0. rewrite -!cats1 !wder_cat => hsub. have hg : (InA sim_dec3 Y (der a f,der a f',a::v)). + by apply: hsub. case: (InA_inv sim3_Eq hg) => [[[g g'] w]] hg1. rewrite /sim3 /sim => [[[ hg2l hg2r] _]]. exists g; exists g'; exists w; split => //. + move => s /=. rewrite (in_der_compat hf2 a s). by apply similar_ok; symmetry. + move => s /=. rewrite (in_der_compat hf3 a s). by apply similar_ok; symmetry. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)