proposition: Theorem filter_ext : forall (A : Set)(ls : list A)(f1 f2 : A -> bool), (forall a, f1 a = f2 a) -> filter f1 ls = filter f2 ls.
proof: Proof. induction ls; intuition; simpl in *. rewrite H. destruct (f2 a); eauto. f_equal; eauto. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1