proposition: Lemma gpred_list_inter : forall E1 E2 l, gpred_list E1 l -> gpred_list E2 l -> gpred_list (Intersection E1 E2) l.
proof: Proof. move => E1 E2. elim => [ | hd tl ih] //=. move => [h1 h1'] [h2 h2']. split. by split. by apply: ih. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)