proposition: Lemma NoDup_length_incl l l' : NoDup l -> length l' <= length l -> incl l l' -> incl l' l.
proof: Proof. intros N. revert l'. induction N as [|a l Hal N IH]. - intro l'; destruct l'; easy. - intros l' E H x Hx. destruct (Add_inv a l') as (l'', AD). { apply H; simpl; auto. } rewrite (Add_in AD) in Hx. simpl in Hx. destruct Hx as [Hx|Hx]; [left; trivial|right]. revert x Hx. apply (IH l''); trivial. * apply Nat.succ_le_mono. now rewrite <- (Add_length AD). * now apply incl_Add_inv with a l'. Qed.
imports: PeanoNat