proposition: Theorem filter_true : forall (A : Set)(ls : list A)(f : A -> bool), (forall a, In a ls -> (f a) = true) -> filter f ls = ls.
proof: Proof. induction ls; intuition; simpl in *. case_eq (f a); intuition. f_equal. eauto. rewrite H in H0. discriminate. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation