proposition: Lemma submseteq_cons_l x l k : x :: l ⊆+ k ↔ ∃ k', k ≡ₚ x :: k' ∧ l ⊆+ k'.
proof: Proof. split. - rewrite submseteq_sublist_l. intros (l'&Hl'&E). rewrite sublist_cons_l in Hl'. destruct Hl' as (k1&k2&?&?); subst. exists (k1 ++ k2). split; eauto using submseteq_inserts_l, sublist_submseteq. by rewrite Permutation_middle. - intros (?&E&?). rewrite E. by constructor. Qed.
imports: stdpp(options)