proposition: Lemma submseteq_app_inv_l l1 l2 k : k ++ l1 ⊆+ k ++ l2 → l1 ⊆+ l2.
proof: Proof. induction k as [|y k IH]; simpl; [done |]. rewrite submseteq_cons_l. intros (?&E%(inj (cons y))&?). apply IH. by rewrite E. Qed.
imports: stdpp(options)