proposition: Lemma l1 : 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) (hd : ldisjoint sim_dec3 X Y), lincl X (build_list_fun_acc ha hp1 hp2 hd).
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] hp1 hp2 /=. - move => _; by apply : lincl_refl. - move => hd. apply: (@lincl_trans _ (X ++ hdY :: tlY)). by apply: lincl_catr; apply: lincl_refl. by apply: hi. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)