proposition: Lemma filter_Permutation : forall (A : Set)(ls1 ls2 : list A)(P : A -> bool), Permutation ls1 ls2 -> Permutation (filter P ls1) (filter P ls2).
proof: Proof. induction 1; intuition; simpl in *. destruct (P x). eapply perm_skip. trivial. trivial. destruct (P x). destruct (P y). eapply perm_swap. eapply Permutation_refl. destruct (P y). eapply Permutation_refl. eapply Permutation_refl. eapply perm_trans; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia