proposition: Lemma InA_Map {A B} eqB : forall (f : A -> B) (b : B) (l : list A), InA eqB b (List.map f l) <-> exists a, eqB b (f a) /\ List.In a l.
proof: Proof. split; induction l; simpl; intros; inversion H; subst; eauto. destruct (IHl H1) as [a' [In_a eq_b]]; eauto. intuition. intuition; subst. constructor; eauto. constructor 2; eauto. 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