proposition: Lemma filter_all_true : forall (A : Set)(ls : list A)(P : A -> bool), (forall a, In a ls -> P a = true) -> filter P ls = ls.
proof: Proof. induction ls; intuition; simpl in *. assert (P a = true). eapply H; intuition. rewrite H0. f_equal; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation