proposition: Lemma InA_map_iff {A B} (f : A -> B) eqv x ls a : f a = x -> (InA eqv x (List.map f ls) <-> InA (fun a b => eqv (f a) (f b)) a ls).
proof: Proof. intro; subst. rewrite !InA_alt. setoid_rewrite in_map_iff. firstorder (subst; 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