proposition: Lemma finite_pred_not : forall E, Finite (set_of_der E) -> Finite (pred_not (set_of_der E)).
proof: Proof. move => E hE. have hsim : Finite (@f_set regexp regexp sim fNot (set_of_der E)). - apply: (@Bar_fun _ _ sim); last done. move => a a'; rewrite /sim /fNot /= => h. by apply similar_congr_Not. apply: (@Bar_gset_incl _ (@f_set regexp regexp sim fNot (set_of_der E))); first done. move => x. rewrite /pred_not. case. move => y [h1 h2]. exists y => //. 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)