Commit 31b00c08 authored by Hai Dang's avatar Hai Dang
Browse files

more to_agreeM lemma

parent 035064c6
......@@ -198,6 +198,18 @@ Proof.
intros. apply agreeM_local_update_fork;
[by apply to_agreeM_included..|apply to_agreeM_valid].
Qed.
Lemma to_agreeM_local_update_fork_singleton m k a :
m !! k = Some a
(to_agreeM m, ε) ~l~> (to_agreeM m, to_agreeM ({[k := a]})).
Proof.
intros.
rewrite (_: ε = to_agreeM ); last first.
{ by rewrite /to_agreeM fmap_empty. }
apply to_agreeM_local_update_fork; [apply map_empty_subseteq|].
by apply map_singleton_subseteq_l.
Qed.
End to_agree.
Arguments agreeMR _ {_ _} _.
......
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