proposition: Lemma rel_map_NoDup : forall (A B : Type)(lsa : list A)(lsb : list B) rel, rel_map rel lsa lsb -> NoDup lsa -> (forall a1 a2 b1 b2, In a1 lsa -> In a2 lsa -> a1 <> a2 -> rel a1 b1 -> rel a2 b2 -> b1 <> b2) -> NoDup lsb.
proof: Proof. induction 1; intuition; simpl in *. econstructor. inversion H1; clear H1; subst. econstructor. eapply ne_all_not_in. intuition. subst. destruct (rel_map_inverse H a'). trivial. intuition. eapply H2. left; eauto. right; eauto. intuition; subst; intuition. eauto. eauto. trivial. eapply IHrel_map; intuition. subst. eapply H2. right. eapply H3. right. eapply H4. trivial. eauto. eauto. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation