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