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