Skip to content
Snippets Groups Projects
Commit f0d5ebf0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename `gmultiset_elem_of_singleton_subseteq` →...

Rename `gmultiset_elem_of_singleton_subseteq` → `gmultiset_singleton_subseteq_l` and swap order to be consistent with Iris's `singleton_included_l`.
parent 9c2d215d
No related branches found
No related tags found
1 merge request!306Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼`
......@@ -568,7 +568,7 @@ Section more_lemmas.
Lemma gmultiset_union_subset_r X Y : X Y X Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_elem_of_singleton_subseteq x X : x X {[+ x +]} X.
Lemma gmultiset_singleton_subseteq_l x X : {[+ x +]} X x X.
Proof. multiset_solver. Qed.
Lemma gmultiset_elem_of_subseteq X1 X2 x : x X1 X1 X2 x X2.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment