proposition: Lemma Permutation_filter2 {A} (l : list A) (p q : A -> bool) : (forall x, xorb (p x) (q x)) -> Permutation l (filter p l ++ filter q l).
proof: Proof. Proof with simpl; intros. intros. induction l; unfold compose; simpl; auto. generalize (H a). case_eq (p a); simpl; intros. apply Permutation_cons; auto. revert H1. case_eq (q a); intros qa; intros; try discriminate. elim H1. apply IHl. revert H1. case_eq (q a); intros qa; intros; try discriminate. auto using Permutation_cons_app. elim H1. Qed.
imports: Program Utf8 Equations.Prop.Equations Bvector List Relations Arith Wf_nat Lia Coq.Lists.SetoidList Coq.Sorting.Sorting Coq.Sorting.Permutation Coq.Sorting.PermutSetoid Bool