proposition: Lemma filter_all_false : forall {A} seq pred, (forall item : A, List.In item seq -> pred item = false) -> List.filter pred seq = [].
proof: Proof. intros A seq pred all_false; induction seq as [ | head tail IH ]; simpl; trivial. rewrite (all_false head) by (simpl; eauto). intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts