proposition: Lemma InA_In_snd : forall {A: Type} (k: key) (e: A) (l : list (key*A)), InA (eq_key_elt (elt:=A)) (k, e) l -> List.In e (List.map snd l).
proof: Proof. intros ? k e ? in_a; rewrite InA_alt, in_map_iff in *; destruct in_a as [(k', e') (eq0, ?)]; destruct eq0; simpl in *; exists (k', e'); intuition. 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