proposition: Lemma bnd_throw s e i (r : cont B) : (def i -> r (Exn e) i) -> verify (bind_s (throw_s A e) s) i r.
proof: Proof. move=>H; apply: bnd_is_try; apply: try_throw; apply: frame0. by rewrite -[i]un0h; apply: val_do=>// y m [->] // [->]; rewrite un0h. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)