proposition: Lemma tryR G A B (s : spec G A) g i j (e : STspec G s) (e1 : A -> ST B) (e2 : exn -> ST B) (f : forall k, form k j) (Q : post B) : (valid i -> (s g).1 i) -> (forall x m, (s g).2 (Val x) m -> vrf (f m) (e1 x) Q) -> (forall x m, (s g).2 (Exn x) m -> vrf (f m) (e2 x) Q) -> vrf (f i) (try e e1 e2) Q.
proof: Proof. move=>Hi H1 H2. apply/vrf_try/(gR _ _ Hi)=>[x|ex] m H V. - by apply: H1 H. by apply: H2. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)