proposition: Theorem NoDup_snd_split_if : forall (A B : Type)(ls : list (A * B)), NoDup (snd (split ls)) -> NoDup ls.
proof: Proof. induction ls; intuition; simpl in *. econstructor. remember (split ls) as z. destruct z. destruct a. simpl in *. inversion H; clear H; subst. econstructor. intuition. eapply in_split_r in H. rewrite <- Heqz in H. simpl in *. intuition. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation