proposition: Lemma bnd_throwR e e1 i (r : post B) : (valid i -> r (Exn e) i) -> vrf i (bind (@throw A e) e1) r.
proof: Proof. by move=>H; apply/vrf_bind/val_throwR. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)