proposition: Theorem NoDup_app_inv_l : forall (l1 l2 : list A), NoDup (l1 ++ l2) -> NoDup l1.
proof: Proof. intros l1; elim l1; simpl in |- *; auto using NoDup_nil. intros a l H l2 H0; inversion H0; apply NoDup_cons; auto. contradict H3; auto with datatypes. apply H with l2; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)