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