proposition: Lemma lminus_pred: forall P l1 l2, gpred_list P l1 -> gpred_list P (lminus l1 l2).
proof: Proof. move => P. elim => [ | hd tl hi] l2 //=. case => hhd htl. case: (InA l2 hd) => //=. - by apply: hi. - by split => //; apply: hi. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)