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

mentioned in merge request !305 (merged)

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

Indeed, they are more widely used by at least a factor of 10 (in my collection of checked-out Iris developments that we have on CI).

LGTM! Needs a changelog though, and ideally a sed script.

added 1 commit

• 5eff5bfd - CHANGELOG.

Compare with previous version

Done.

resolved all threads

added 1 commit

• 186412a7 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

LGTM. Don't forget the ping. :)

I do that tomorrow when I can fix reverse dependencies.

approved this merge request

mentioned in commit e263eb10

merged

@iris-users This is a breaking change:

Rename gmultiset_elem_of_singleton_subseteq → gmultiset_singleton_subseteq_l and swap the equivalence to be consistent with Iris's singleton_included_l.

mentioned in merge request !308 (merged)