Skip to content

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

Robbert Krebbers requested to merge robbert/singleton_subseteq into master

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

Merge request reports