Require Export ConcreteExecution.

Definition cupdate_store_(f: store -> store): cmutatora store :=
  fun st => let (s, h) := st in
  single (f s, h) s.

Lemma cwith_store_covers_cupdate_store_ s A (C: cmutatora A):
  cwith_store s C '_x">==> s0 <- cupdate_store_ (fun _ => s); C;, cupdate_store_ (fun _ => s0).

Lemma cupdate_store__covers_cwith_store s A (C: cmutatora A):
  s0 <- cupdate_store_ (fun _ => s); C;, cupdate_store_ (fun _ => s0) '_x">==> cwith_store s C.