proposition: Lemma NoDup_submseteq l k : NoDup l → (∀ x, x ∈ l → x ∈ k) → l ⊆+ k.
proof: Proof. intros Hl. revert k. induction Hl as [|x l Hx ? IH]. { intros k Hk. by apply submseteq_nil_l. } intros k Hlk. destruct (elem_of_list_split k x) as (l1&l2&?); subst. { apply Hlk. by constructor. } rewrite <-Permutation_middle. apply submseteq_skip, IH. intros y Hy. rewrite elem_of_app. specialize (Hlk y). rewrite elem_of_app, !elem_of_cons in Hlk. by destruct Hlk as [?|[?|?]]; subst; eauto. Qed.
imports: stdpp(options)