proposition: Lemma mem_filter: forall x l, (InA (filter P l) x) = (P x) && (InA l x).
proof: Proof. move => x; elim => [ | hd tl ] //=. - by rewrite andbF. - case: eqA_dec => /=. + move => heq. rewrite (P_compat heq). case: (P hd) => //=. by case: eqA_dec => //=. + case: (P hd) => //=. by case: eqA_dec => //=. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)