proposition: Lemma submseteq_sublist_r l1 l3 : l1 ⊆+ l3 ↔ ∃ l2, l1 ≡ₚ l2 ∧ l2 `sublist_of` l3.
proof: Proof. rewrite submseteq_sublist_l. split; intros (l2&?&?); eauto using sublist_Permutation, Permutation_sublist. Qed.
imports: stdpp(options)