proposition: Lemma val_readR v x i (f : update (x :-> v) i) (r : cont A) : (def f -> r (Val v) f) -> verify (read_s A x) f r.
proof: Proof. by rewrite updateE; apply: val_read. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps rels stmod stsep stlog)