proposition: Lemma filter_eq : forall (A : Set)(ls : list A)(P1 P2 : A -> bool), (forall a, In a ls -> P1 a = P2 a) -> filter P1 ls = filter P2 ls.
proof: Proof. induction ls; intuition; simpl in *. rewrite (H a); intuition. destruct (P2 a). f_equal. eapply IHls; intuition. eapply IHls; intuition. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF