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