proposition: Lemma submseteq_cons_r x l k : l ⊆+ x :: k ↔ l ⊆+ k ∨ ∃ l', l ≡ₚ x :: l' ∧ l' ⊆+ k.
proof: Proof. split. - rewrite submseteq_sublist_r. intros (l'&E&Hl'). rewrite sublist_cons_r in Hl'. destruct Hl' as [?|(?&?&?)]; subst. + left. rewrite E. eauto using sublist_submseteq. + right. eauto using sublist_submseteq. - intros [?|(?&E&?)]; [|rewrite E]; by constructor. Qed.
imports: stdpp(options)