proposition: Lemma vrf_throw i (Q : post A) : (valid i -> Q (Exn e) i) -> vrf i throw Q.
proof: Proof. by move=>H V; exists I=>_ _ [->->]; apply: H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)