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