Commit 42ecd0a6 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Stronger delete_option_local_update

parent 36f74ae4
...@@ -166,9 +166,8 @@ Proof. ...@@ -166,9 +166,8 @@ Proof.
destruct z as [z|]; last done. destruct y; inversion Heq. destruct z as [z|]; last done. destruct y; inversion Heq.
Qed. Qed.
Lemma delete_option_local_update {A : cmraT} (x y : A) : Lemma delete_option_local_update {A : cmraT} (x : option A) (y : A) :
Exclusive y Exclusive y (x, Some y) ~l~> (None, None).
(Some x, Some y) ~l~> (None, None).
Proof. Proof.
move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done. move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
destruct z as [z|]; last done. exfalso. destruct z as [z|]; last done. exfalso.
......
Markdown is supported
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