Add several lemmas about list singletons
There already is a lemma
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.
A lemma that establishes the necessary and sufficient condition for a singleton to be included in another list.