Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼`

See discussion in !305 (comment 71807)

I decided to use Iris's names and argument because:

• It's shorter
• Iris's singleton_included lemmas have been there for longer than the multiset lemmas, so are (probably) more widely used