proposition: Lemma val_ret v i (r : cont A) : (def i -> r (Val v) i) -> verify (ret_s v) i r.
proof: Proof. by rewrite -[i]un0h=>H; apply: val_do=>// x m [->] // [->]. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)