proposition: Lemma filter_union : forall P s1 s2 P_compat, eq_set (filter P (union s1 s2) P_compat) (union (filter P s1 P_compat) (filter P s2 P_compat)).
proof: Proof. intros P [l1 wr1] [l2 wr2] P_compat e; split; unfold mem; simpl. intro H; destruct (filter_2_list _ _ _ P_compat H) as [H' Pe]; destruct (union_12_aux _ _ _ H'); [ apply union_1_aux | apply union_2_aux] ; apply filter_1_list; trivial. intro H; destruct (union_12_aux _ _ _ H) as [ H' | H']; destruct (filter_2_list _ _ _ P_compat H') as [H'' Pe]; apply filter_1_list; trivial; [ apply union_1_aux | apply union_2_aux] ; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)