Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼` (!306) · Merge requests · Iris / stdpp

Merged Robbert Krebbers requested to merge robbert/singleton_subseteq into master 3 years ago

Status	Pipeline	Stages
Passed 00:05:01 3 years ago	Apply 1 suggestion(s) to 1 file(s) #51143 306 186412a7	Stage: build	Download artifacts No artifacts found
Passed 00:05:00 3 years ago	CHANGELOG. #51142 306 5eff5bfd	Stage: build	Download artifacts No artifacts found
Passed 00:05:01 3 years ago	Add `singleton_subseteq_l` and `singleton_subseteq`. #51140 306 7921671c	Stage: build	Download artifacts No artifacts found

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