proposition: Lemma gpred_list_cat : forall l1 l2 (E:gset A), (gpred_list E l1 /\ gpred_list E l2) <-> gpred_list E (l1++l2).
proof: Proof. elim => [ | hd tl hi] l2 E //=; split => //. - by case. - case => [[h1 h2]] h3; split => //. case: (hi l2 E) => h _. by apply: h. - case => h1 h2. case: (hi l2 E) => _ h. split. split => //. by apply h. by apply h. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)