proposition: Lemma sublist_alt l1 l2 : l1 `sublist_of` l2 ↔ ∃ is, l1 = foldr delete l2 is.
proof: Proof. split; [|intros [is ->]; apply sublist_foldr_delete]. intros Hl12. cut (∀ k, ∃ is, k ++ l1 = foldr delete (k ++ l2) is). { intros help. apply (help []). } induction Hl12 as [|x l1 l2 _ IH|x l1 l2 _ IH]; intros k. - by eexists []. - destruct (IH (k ++ [x])) as [is His]. exists is. by rewrite <-!(assoc_L (++)) in His. - destruct (IH k) as [is His]. exists (is ++ [length k]). rewrite fold_right_app. simpl. by rewrite delete_middle. Qed.
imports: stdpp(options)