proposition: Lemma Injective_list_carac A B (d:decidable_eq A)(f:A->B) : Injective f <-> (forall l, NoDup l -> NoDup (map f l)).
proof: Proof. split. - intros. now apply Injective_map_NoDup. - intros H x y E. destruct (d x y); trivial. assert (N : NoDup (x::y::nil)). { repeat constructor; simpl; intuition. } specialize (H _ N). simpl in H. rewrite E in H. inversion_clear H; simpl in *; intuition. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec