proposition: Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist_of` k ++ l2 → l1 `sublist_of` l2.
proof: Proof. induction k as [|y k IH]; simpl; [done |]. rewrite sublist_cons_r. intros [Hl12|(?&?&?)]; [|simplify_eq; eauto]. rewrite sublist_cons_l in Hl12. destruct Hl12 as (k1&k2&Hk&?). apply IH. rewrite Hk. eauto using sublist_inserts_l, sublist_cons. Qed.
imports: stdpp(options)