proposition: Lemma sublist_Permutation l1 l2 l3 : l1 `sublist_of` l2 → l2 ≡ₚ l3 → ∃ l4, l1 ≡ₚ l4 ∧ l4 `sublist_of` l3.
proof: Proof. intros Hl1l2 Hl2l3. revert l1 Hl1l2. induction Hl2l3 as [|x l2 l3 ? IH|x y l2|l2 l2' l3 ? IH1 ? IH2]. - intros l1. by exists l1. - intros l1. rewrite sublist_cons_r. intros [?|(l1'&l1''&?)]; subst. { destruct (IH l1) as (l4&?&?); trivial. exists l4. split. - done. - by constructor. } destruct (IH l1') as (l4&?&Hl4); auto. exists (x :: l4). split; [ by constructor | by constructor ]. - intros l1. rewrite sublist_cons_r. intros [Hl1|(l1'&l1''&Hl1)]; subst. { exists l1. split; [done|]. rewrite sublist_cons_r in Hl1. destruct Hl1 as [?|(l1'&?&?)]; subst; by repeat constructor. } rewrite sublist_cons_r in Hl1. destruct Hl1 as [?|(l1''&?&?)]; subst. + exists (y :: l1'). by repeat constructor. + exists (x :: y :: l1''). by repeat constructor. - intros l1 ?. destruct (IH1 l1) as (l3'&?&?); trivial. destruct (IH2 l3') as (l3'' &?&?); trivial. exists l3''. split; [|done]. etrans; eauto. Qed.
imports: stdpp(options)