proposition: Lemma map_filter_all_false : forall {A} pred seq, (forall subseq, List.In subseq seq -> forall (item: A), List.In item subseq -> pred item = false) -> (List.map (List.filter pred) seq) = (List.map (fun x => []) seq).
proof: Proof. intros A pred seq all_false; induction seq as [ | subseq subseqs IH ] ; simpl; trivial. f_equal. specialize (all_false subseq (or_introl eq_refl)). apply filter_all_false; assumption. apply IH; firstorder. 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