proposition: Theorem NoDup_app : forall l1 l2, NoDup l1 -> NoDup l2 -> (forall a : A, In a l1 -> In a l2 -> False) -> NoDup (l1 ++ l2).
proof: Proof. intros L1; elim L1; simpl in |- *; auto. intros a l H l2 H0 H1 H2; apply NoDup_cons; simpl in |- *; auto. red in |- *; intros H3; case in_app_or with (1 := H3); auto; intros H4. inversion H0; auto. apply H2 with a; auto. apply H; auto. apply NoDup_cons_iff with (1 := H0); auto. intros a0 H3 H4; apply (H2 a0); auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)