proposition: Lemma gpred_list_notinP : forall (l:seq A) a, reflect (gpred_list (neq eqA a) l) (~~ InA l a).
proof: Proof. elim => [ a | hd tl hi a] //=. by apply (iffP idP). apply (iffP idP). - case: (eqA_dec a hd) => //=. move => hn1 hn2. split => //. by apply/hi. - move => [ h1 h2]. case: (eqA_dec a hd) => /=. move => h. by case: h1. move => h. by apply/hi. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)