proposition: Lemma filter_eq_self_of_mem_implies_P : forall l P, (forall x, mem x l -> P x) -> filter P l = l.
proof: Proof. Proof using. induction l; introv M. { auto. } { rewrite filter_cons. case_if. { fequals. applys IHl. introv Mx. applys* M. } { false* M. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)