proposition: Lemma subset_filter : forall (P1 P2 : A -> bool) s1 s2 P1_compat P2_compat, subset s1 s2 -> (forall e, P1 e = true -> P2 e = true) -> subset (filter P1 s1 P1_compat) (filter P2 s2 P2_compat).
proof: Proof. intros P1 P2 s1 s2 P1_compat P2_compat Hs HP e H. apply filter_1. apply (Hs e). apply (proj1 (filter_2 _ _ P1_compat _ H)). apply HP. apply (proj2 (filter_2 _ _ P1_compat _ H)). Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)