proposition: Lemma forall_in_map_snd_eq_key_elt {A} ls (P : _ -> Prop) : (forall x : A, List.In x (List.map (@snd _ _) ls) -> P x) <-> (forall x : key * A, InA (@eq_key_elt A) x ls -> P (snd x)).
proof: Proof. rewrite <- forall_in_eq_key_elt_snd. setoid_rewrite in_map_iff. setoid_rewrite ex_eq_snd_and. setoid_rewrite ex_ind_iff. split; intro H; [ intros [k x]; specialize (H x k) | intros x k; specialize (H (k, x)) ]; assumption. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances