proposition: Lemma submseteq_sublist_l l1 l3 : l1 ⊆+ l3 ↔ ∃ l2, l1 `sublist_of` l2 ∧ l2 ≡ₚ l3.
proof: Proof. split. { intros Hl13. elim Hl13; clear l1 l3 Hl13. - by eexists []. - intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor. - intros x y l. exists (y :: x :: l). by repeat constructor. - intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor. - intros l1 l3 l5 ? (l2&?&?) ? (l4&?&?). destruct (Permutation_sublist l2 l3 l4) as (l3'&?&?); trivial. exists l3'. split; etrans; eauto. } intros (l2&?&?). trans l2; auto using sublist_submseteq, Permutation_submseteq. Qed.
imports: stdpp(options)