proposition: Lemma val_writeR (v : A) (w : B) x i (f : forall k, update k i) (r : cont unit) : (def (f (x :-> v)) -> r (Val tt) (f (x :-> v))) -> verify (write_s x v) (f (x :-> w)) r.
proof: Proof. by rewrite !updateE; apply: val_write. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps rels stmod stsep stlog)