proposition: Lemma filter_union : forall {A: Type} (seq1 seq2: list A), forall (pred: A -> bool), SetEq (List.filter pred (SetUnion seq1 seq2)) (SetUnion (List.filter pred seq1) (List.filter pred seq2)).
proof: Proof. unfold SetEq, SetUnion; split; intros; rewrite filter_In, in_app_iff in *; rewrite ! filter_In in *; tauto. Qed.
imports: Coq.Lists.List Coq.Bool.Bool Coq.Structures.OrderedType Coq.Classes.Morphisms Coq.Setoids.Setoid Fiat.Common.Coq__8_4__8_5__Compat