proposition: Lemma l4 : forall (E F:bregexp), forall (X Y:seq (bregexp*bregexp*bword)) (ha : Acc (gpred_list (Prod (set_pair_der E F) bT)) (sup sim3) X) (hp1 : gpred_list (Prod (set_pair_ders E F) bT) X) (hp2 : gpred_list (Prod (set_pair_ders E F) bT) Y) (hs: ldisjoint sim_dec3 X Y), gpred_list (ff E F) X -> gpred_list (ff E F) Y -> gpred_list (ff E F) (build_list_fun_acc ha hp1 hp2 hs).
proof: Proof. move => E F X Y ha. move: Y. elim ha using Acc_rect_dep. clear X ha. move => X hp hi [ | hdY tlY] hhp1 hp2 hs /=. - by move => h _. - move => hX hY. apply: hi. apply/gpred_list_cat; split => //. apply: lminus_pred. clear hp2 hs. case: hdY hY => [[hdl hdr] s] []. rewrite {1}/ff => [[h1 h2]] h3 /=; split. + rewrite !rev_cons !wder_rcons. split. move => w. by apply in_der_compat. move => w. by apply in_der_compat. split. + rewrite !rev_cons !wder_rcons. split. move => w. by apply in_der_compat. move => w. by apply in_der_compat. + by apply: DER_preserves_lang. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)