proposition: Lemma submseteq_app_l l1 l2 k : l1 ++ l2 ⊆+ k ↔ ∃ k1 k2, k ≡ₚ k1 ++ k2 ∧ l1 ⊆+ k1 ∧ l2 ⊆+ k2.
proof: Proof. split. - rewrite submseteq_sublist_l. intros (l'&Hl'&E). rewrite sublist_app_l in Hl'. destruct Hl' as (k1&k2&?&?&?); subst. exists k1, k2. split; [done|]. eauto using sublist_submseteq. - intros (?&?&E&?&?). rewrite E. eauto using submseteq_app. Qed.
imports: stdpp(options)