fact: Parameter vrf_try : forall A B (e : ST A) (e1 : A -> ST B) (e2 : exn -> ST B) i (Q : post B), vrf i e (fun x m => match x with | Val x' => vrf m (e1 x') Q | Exn ex => vrf m (e2 ex) Q end) -> vrf i (try e e1 e2) Q.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)