proposition: Lemma val_write (v : A) (w : B) x i (r : cont unit) : (def (x :-> v :+ i) -> r (Val tt) (x :-> v :+ i)) -> verify (write_s x v) (x :-> w :+ i) r.
proof: Proof. move=>*; apply: val_do; first by [exists B; exists w]; by move=>y m [// [->] ->]. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)