proposition: Lemma finite_pred_scalar : forall P F, Finite P -> Finite (pred_scalar P F).
proof: Proof. move => P F hdP. have hsim : Finite (@f_set (regexp*regexp) regexp sim fConc (Prod P (pred_singl F))). - apply : (@Bar_fun _ _ (eq_prod sim sim)). + move => [a1 b1] [a2 b2]. case. rewrite /sim /fConc /=. move => h1 h2. by apply similar_congr_Conc. apply : (@Bar_grel_incl _ _ (r_prod nsim nsim)). apply: Bar_gset_prod; first done. apply finite_pred_singl. 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 fConc (Prod P (pred_singl F)))); first done. move => x. case. move => y [hl hr]. rewrite /f_set. exists (y,F). split => //. rewrite /pred_singl. reflexivity. rewrite /sim /fConc. 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)