proposition: Lemma try_do (s : spec A) s1 s2 i j (r : cont B) : s.1 i -> (forall x m, s.2 (Val x) i m -> verify (s1 x) (m :+ j) r) -> (forall e m, s.2 (Exn e) i m -> verify (s2 e) (m :+ j) r) -> verify (try_s s s1 s2) (i :+ j) r.
proof: Proof. move=>H1 H2 H3; apply: frame0=>D; split=>[|y m]. - split; first by apply: fr_pre; exists i; exists empty; rewrite unh0. by split=>y m; case/(_ i j (erefl _) D H1)=>m1 [->][D2]; [case/H2 | case/H3]. by case=>[[x]|[e]][h][]; case/(_ i j (erefl _) D H1)=>m1 [->][D2]; [case/H2 | case/H3]=>// _; apply. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)