proposition: Lemma nodup_app: forall (A: Type) (l1 l2: list A), NoDup (l1 ++ l2) <-> NoDup l1 /\ NoDup l2 /\ disjoint l1 l2.
proof: Proof. induction l1; intros. - split. * simpl; split; auto using NoDup_nil. split; auto. unfold disjoint; intuition. * simpl; intros. destruct H. destruct H0. assumption. - simpl. rewrite nodup_cons. rewrite IHl1. rewrite In_app. unfold disjoint. split; intuition (subst; eauto). * apply NoDup_cons; auto. * inversion IN1; subst; auto. eauto. * inversion H0; subst; auto. * inversion H0; subst. specialize (H2 a). apply H2; auto. left; auto. * inversion H0; auto. * specialize (H2 a0). apply H2; auto. right; auto. Qed.
imports: Coq(List Permutation)