proposition: Lemma tryX G A B (s : spec G A) g (m : heapPCM) m0 j tm k wh r2 (e : STspec G s) (e1 : A -> ST B) (e2 : exn -> ST B) (fm : Syntactify.form (empx _) j tm) (fu : uform m0 (Syntactify.untag fm)) (f : forall q, form q r2) (fg : PullX.rform j k tm wh (Some (untag (heap_of (f m0))))) (Q : post B) : untagU fu = m -> (valid m -> (s g).1 m) -> (forall v n, (s g).2 (Val v) n -> vrf (f n) (e1 v) Q) -> (forall x n, (s g).2 (Exn x) n -> vrf (f n) (e2 x) Q) -> vrf (fg : heapPCM) (try e e1 e2) Q.
proof: Proof. move=>Hm Hp Hv Hx. by apply/vrf_try/(gX _ _ Hm Hp)=>[x|ex] n H V; [apply: Hv|apply: Hx]. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)