proposition: Theorem NoDup_app : forall (A : Type)(ls1 ls2 : list A), NoDup (ls1 ++ ls2) -> NoDup ls1 /\ NoDup ls2 /\ (forall a1 a2, In a1 ls1 -> In a2 ls2 -> a1 <> a2).
proof: Proof. induction ls1; intros; simpl in *. intuition. econstructor. inversion H; clear H; subst. eapply IHls1 in H3. intuition. econstructor. intuition. trivial. subst. eapply H2. eapply in_or_app. intuition. subst. eapply H3; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation