proposition: Theorem NoDup_app_inv : forall l1 l2 (a : A), NoDup (l1 ++ l2) -> In a l1 -> In a l2 -> False.
proof: Proof. intros l1; elim l1; simpl in |- *; auto. intros a l H l2 a0 H0 [H1| H1] H2. inversion H0; auto. case H5; rewrite H1; auto with datatypes. apply (H l2 a0); auto. apply NoDup_cons_iff with (1 := H0); auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)