proposition: Lemma singleton_submseteq_l l x : [x] ⊆+ l ↔ x ∈ l.
proof: Proof. split. - intros Hsub. eapply elem_of_submseteq; [|done]. apply elem_of_list_singleton. done. - intros (l1&l2&->)%elem_of_list_split. apply submseteq_cons_middle, submseteq_nil_l. Qed.
imports: stdpp(options)