proposition: Lemma filter_union : forall P P_dec s1 s2, eq_set (filter P P_dec (union s1 s2)) (union (filter P P_dec s1) (filter P P_dec s2)).
proof: Proof. intros P P_dec [l1 wr1] [l2 wr2] e; split; unfold mem, union, support; simpl; generalize l1 e; clear l1 wr1 wr2 e; induction l2 as [ | e2 l2]; intros l1 e; trivial. intro H; simpl in H; destruct (In_dec eq_elt_dec e2 l1) as [e2_in_l1 | e2_not_in_l1]. simpl; destruct (P_dec e2) as [P_e2 | not_P_e2]. simpl; destruct (In_dec eq_elt_dec e2 (filter_aux P P_dec l1)) as [e2_in_l1_and_P_e2 | not_e2_in_l1_and_P_e2]. intros; apply IHl2; trivial. absurd (In e2 (filter_aux P P_dec l1)); trivial; refine (filter_1_list _ _ _ _ _ _); trivial. intros; apply IHl2; trivial. generalize (IHl2 _ _ H); simpl; destruct (P_dec e2) as [P_e2 | not_P_e2]. simpl; destruct (In_dec eq_elt_dec e2 (filter_aux P P_dec l1)) as [e2_in_l1_and_P_e2 | not_e2_in_l1_and_P_e2]; [idtac | trivial]. absurd (In e2 l1); trivial; generalize (filter_2_list _ _ _ _ e2_in_l1_and_P_e2); intuition. trivial. simpl; destruct (P_dec e2) as [P_e2 | not_P_e2]. destruct (In_dec eq_elt_dec e2 l1) as [e2_in_l1 | e2_not_in_l1]. simpl; destruct (In_dec eq_elt_dec e2 (filter_aux P P_dec l1)) as [e2_in_l1_and_P_e2 | not_e2_in_l1_and_P_e2]. intros; apply IHl2; trivial. absurd (In e2 (filter_aux P P_dec l1)); trivial; refine (filter_1_list _ _ _ _ _ _); trivial. generalize (IHl2 (e2 :: l1) e); simpl; destruct (P_dec e2) as [_ | not_P_e2]. destruct (In_dec eq_elt_dec e2 (filter_aux P P_dec l1)) as [e2_in_l1_and_P_e2 | not_e2_in_l1_and_P_e2]; [idtac | trivial]. absurd (In e2 l1); trivial; generalize (filter_2_list _ _ _ _ e2_in_l1_and_P_e2); intuition. absurd (P e2); trivial. destruct (In_dec eq_elt_dec e2 l1) as [ e2_in_l1 | e2_not_in_l1 ]. intro; apply IHl2; trivial. intro H; refine (IHl2 (e2 :: l1) e _); destruct (union_12_aux _ _ _ H) as [ H1 | H2 ]. apply union_1_aux; simpl; destruct (P_dec e2) as [ P_e2 | _]; trivial; absurd (P e2); trivial. apply union_2_aux; trivial. Qed.
imports: List more_list list_permut Arith