proposition: Lemma map_inj {A B : Type} (f : A → B) (f_inj : ∀ x y, f x = f y → x = y) xs ys : List.map f xs = List.map f ys → xs = ys.
proof: Proof. generalize dependent ys. induction xs, ys; simpl; intros; auto; try inv H. apply f_inj in H1; subst. f_equal. now apply IHxs. Qed.
imports: Coq.Lists.List Category.Lib.Tactics