proposition: Lemma app_NoDup : forall(A : Set)(ls1 ls2 : list A), NoDup ls1 -> NoDup ls2 -> (forall a, In a ls1 -> ~In a ls2) -> (forall a, In a ls2 -> ~In a ls1) -> NoDup (ls1 ++ ls2).
proof: Proof. induction ls1; intuition. inversion H; clear H; subst. rewrite <- app_comm_cons. econstructor. intuition. eapply in_app_or in H. intuition. eapply H1. simpl. left. eauto. trivial. eapply IHls1; eauto. intuition. eapply H1. simpl. right. eauto. eauto. intuition. eapply H1. simpl. right. eauto. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation