proposition: Lemma finite_pred_plus : forall E F, Finite (set_of_der E) -> Finite (set_of_der F) -> Finite (pred_plus (set_of_der E) (set_of_der F)).
proof: Proof. move => E F hE hF. have hsim : Finite (@f_set (regexp*regexp) regexp sim fPlus (Prod (set_of_der E) (set_of_der F))). - apply: (@Bar_fun _ _ (eq_prod sim sim)). + move => [a1 b1] [a2 b2]. case. rewrite /sim /fPlus /=. move => h1 h2; by apply similar_congr_Plus. apply : (@Bar_grel_incl _ _ (r_prod nsim nsim)). by apply: Bar_gset_prod. move => [a1 b1] [a2 b2]. rewrite /nsim /neq /eq_prod /r_prod /sim. case: (similar a1 a2) => h. right. move => h'. apply :h. by split. by left. apply: (@Bar_gset_incl _ (f_set sim fPlus (Prod (set_of_der E) (set_of_der F)))); first done. move => x. rewrite /In /f_set /pred_plus. case. move => y. move => [R []]. move => h1 [h2 h3]. exists (y,R). by split. by symmetry. Qed.
imports: Coq(RelationClasses Setoid Morphisms Permutation) Coq(SetoidList Mergesort Orders) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp)