proposition: Lemma in_map_iff_injective {A B} (f : A -> B) (l : list A) (y : A) (f_injective : forall x, f x = f y -> x = y) : In (f y) (map f l) <-> In y l.
proof: Proof. split; intro H. { apply in_map_iff in H. destruct H as [x [H H']]. apply f_injective in H. subst; assumption. } { apply in_map_iff. exists y; split; trivial. } Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Common