proposition: Lemma filter_2 : forall (P_bool : A -> bool) s P_compat e, mem e (filter P_bool s P_compat) -> mem e s /\ P_bool e = true.
proof: Proof. unfold mem, support; intros P_bool [l wr] e E e_in_l_and_P_e. apply filter_2_list; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)