proposition: Lemma filter_not_In : forall (A : Set)(ls : list A)(P : A -> bool) a, (~In a ls) \/ P a = false <-> ~In a (filter P ls).
proof: Proof. intuition. eapply H1. eapply filter_In; eauto. assert (P a = true -> False). intuition. congruence. eapply H. eapply filter_In; eauto. case_eq (P a); intuition. left. intuition. eapply H. eapply filter_In; eauto. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec