proposition: Lemma map_snd {A B C} : forall (f : A -> B) (l : list (C * A)), List.map f (List.map snd l) = List.map snd (List.map (fun ca => (fst ca, f (snd ca))) l).
proof: Proof. intros; repeat rewrite List.map_map; induction l; simpl; eauto. 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