Commit edfbdd5f authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Readd core_id_local_update

parent 9ff3a924
......@@ -59,6 +59,14 @@ Section updates.
destruct mz as [z|]; [|done]. by destruct (id_freeN_r n n x z).
Qed.
Lemma core_id_local_update x y z `{!CoreId y} :
y x (x, z) ~l~> (x, z y).
Proof.
intros Hincl n mf ? Heq; simpl in *; split; first done.
rewrite [x]core_id_extract // Heq. destruct mf as [f|]; last done.
simpl. rewrite -assoc [f y]comm assoc //.
Qed.
Lemma local_update_discrete `{!CmraDiscrete A} (x y x' y' : A) :
(x,y) ~l~> (x',y') mz, x x y ? mz x' x' y' ? mz.
Proof.
......
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