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