proposition: Lemma bnd_readR e v x i (f : form (x :-> v) i) (r : post B) : vrf f (e v) r -> vrf f (bind (@read A x) e) r.
proof: Proof. by move=>H; apply/vrf_bind/val_readR. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)