proposition: Lemma filter_2 : forall (P : elt -> Prop) P_dec s e, mem e (filter P P_dec s) -> mem e s /\ P e.
proof: Proof. unfold mem, support; intros P P_dec [l wr] e e_in_l_and_P_e; apply filter_2_list with P_dec; trivial. Qed.
imports: List more_list list_permut Arith