proposition: Lemma Permutation_sublist l1 l2 l3 : l1 ≡ₚ l2 → l2 `sublist_of` l3 → ∃ l4, l1 `sublist_of` l4 ∧ l4 ≡ₚ l3.
proof: Proof. intros Hl1l2. revert l3. induction Hl1l2 as [|x l1 l2 ? IH|x y l1|l1 l1' l2 ? IH1 ? IH2]. - intros l3. by exists l3. - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst. destruct (IH l3'') as (l4&?&Hl4); auto. exists (l3' ++ x :: l4). split. + by apply sublist_inserts_l, sublist_skip. + by rewrite Hl4. - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?& Hl3); subst. rewrite sublist_cons_l in Hl3. destruct Hl3 as (l5'&l5''&?& Hl5); subst. exists (l3' ++ y :: l5' ++ x :: l5''). split. + by do 2 apply sublist_inserts_l, sublist_skip. + by rewrite !Permutation_middle, Permutation_swap. - intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial. destruct (IH1 l3') as (l3'' &?&?); trivial. exists l3''. split; [done|]. etrans; eauto. Qed.
imports: stdpp(options)