Commit 0a21dfda authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ralf/singleton_mono' into 'master'

add singleton_mono

See merge request iris/iris!606
parents afe51813 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 ]}.
......
Supports Markdown
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