proposition: Lemma filter_flat_map_join_snd : forall {A B} f s1 s2, flat_map (filter (fun x : A * B => f (snd x))) (map (fun a1 : A => map (fun b : B => (a1, b)) s2) s1) = flat_map (fun a1 : A => map (fun b : B => (a1, b)) (filter f s2)) s1.
proof: Proof. induction s1; simpl; intros; trivial. rewrite IHs1; f_equiv. rewrite filter_map; simpl; reflexivity. 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