list_lookup_singletonM_{lt,gt}
There already is a lemma list_lookup_singletonM_ne: https://gitlab.mpi-sws.org/iris/iris/blob/9014fab06c25ac9b2d2a733f225e1cdf56d9d654/theories/algebra/list.v#L372-374
However, whether something is a ε or a Some ε is significant in some cases—for example, when comparing two lists, which is done element-by-element.
list_singletonM_included
A lemma that establishes the necessary and sufficient condition for a singleton to be included in another list.