proposition: Lemma try_gh (r : cont B) : let: s := (fun i => exists x, i \In p x, fun y i m => forall x, i \In p x -> q x y i m) in (forall x m, q t (Val x) i m -> verify (s1 x) (m :+ j) r) -> (forall e m, q t (Exn e) i m -> verify (s2 e) (m :+ j) r) -> i \In p t -> verify (try_s s s1 s2) (i :+ j) r.
proof: Proof. by move=>*; apply: try_do=>/=; eauto. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)