proposition: Lemma sublist_app_l l1 l2 k : l1 ++ l2 `sublist_of` k ↔ ∃ k1 k2, k = k1 ++ k2 ∧ l1 `sublist_of` k1 ∧ l2 `sublist_of` k2.
proof: Proof. split. - revert l2 k. induction l1 as [|x l1 IH]; intros l2 k; simpl. { eexists [], k. by repeat constructor. } rewrite sublist_cons_l. intros (k1 & k2 &?&?); subst. destruct (IH l2 k2) as (h1 & h2 &?&?&?); trivial; subst. exists (k1 ++ x :: h1), h2. rewrite <-(assoc_L (++)). auto using sublist_inserts_l, sublist_skip. - intros (?&?&?&?&?); subst. auto using sublist_app. Qed.
imports: stdpp(options)