proposition: Lemma sublist_app_inv_r k l1 l2 : l1 ++ k `sublist_of` l2 ++ k → l1 `sublist_of` l2.
proof: Proof. revert l1 l2. induction k as [|y k IH]; intros l1 l2. { by rewrite !(right_id_L [] (++)). } intros. opose proof* (IH (l1 ++ [_]) (l2 ++ [_])) as Hl12. { by rewrite <-!(assoc_L (++)). } rewrite sublist_app_l in Hl12. destruct Hl12 as (k1&k2&E&?&Hk2). destruct k2 as [|z k2] using rev_ind; [inv Hk2|]. rewrite (assoc_L (++)) in E; simplify_list_eq. eauto using sublist_inserts_r. Qed.
imports: stdpp(options)