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