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