proposition: Lemma finite_der_And : forall E F, Finite (set_of_der E) -> Finite (set_of_der F) -> Finite (set_of_der (And E F)).
proof: Proof. move => E F hE hF. apply: (@Bar_gset_incl _ (pred_and (set_of_der E) (set_of_der F))). by apply : finite_pred_and. by apply: incl_der_pred_and. 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)