proposition: Lemma filter_1 : forall (P : elt -> Prop) P_dec s e, mem e s -> P e -> mem e (filter P P_dec s).
proof: Proof. unfold mem, support; intros P P_dec [l wr] e e_in_s P_e; simpl; apply filter_1_list; trivial. Qed.
imports: List more_list list_permut Arith