Skip to content
Snippets Groups Projects
Commit 2d1fb3d0 authored by Ralf Jung's avatar Ralf Jung
Browse files

add singleton_mono

parent 4884e2e9
No related branches found
No related tags found
1 merge request!606add singleton_mono
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 0 deletions
iris/algebra/gmap.v
+ 3
− 0
View file @ 2d1fb3d0
...@@ -349,6 +349,9 @@ Proof. ...@@ -349,6 +349,9 @@ Proof.
apply Some_included. by rewrite Hi. apply Some_included. by rewrite Hi.
- intros ?. exists y. by rewrite lookup_insert Some_included. - intros ?. exists y. by rewrite lookup_insert Some_included.
Qed. Qed.
Lemma singleton_mono i x y :
x ≼ y → {[ i := x ]} ≼ ({[ i := y ]} : gmap K A).
Proof. intros Hincl. apply singleton_included. right. done. Qed.
Global Instance singleton_cancelable i x : Global Instance singleton_cancelable i x :
Cancelable (Some x) → Cancelable {[ i := x ]}. Cancelable (Some x) → Cancelable {[ i := x ]}.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment