proposition: Lemma filter_pred_eq : forall (A : Set)(p1 p2 : A -> bool)(ls : list A), (forall a, In a ls -> p1 a = p2 a) -> filter p1 ls = filter p2 ls.
proof: Proof. induction ls; intuition; simpl in *. rewrite H. destruct (p2 a); intuition. f_equal. intuition. intuition. Qed.
imports: Crypto FCF RndNat Asymptotic