proposition: Lemma app_NoDup_inv : forall (A : Set)(ls1 ls2 : list A), NoDup (ls1 ++ ls2) -> (forall a, In a ls1 -> In a ls2 -> False).
proof: Proof. induction ls1; intuition; simpl in *. intuition. subst. inversion H; clear H; subst. eapply H3. eapply in_or_app. intuition. inversion H; clear H; subst. eapply IHls1; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation