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