proposition: Theorem NoDup_app_inv_r : forall l1 l2 : list A, NoDup (l1 ++ l2) -> NoDup l2.
proof: Proof. intros l1; elim l1; simpl in |- *; auto. intros a l H l2 H0; inversion H0; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)