proposition: Lemma bnd_ret s (v : A) i (r : cont B) : verify (s v) i r -> verify (bind_s (ret_s v) s) i r.
proof: Proof. by move=>H; apply: bnd_is_try; apply: try_ret. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)