proposition: Lemma gE G A (s : spec G A) g i (e : @STspec G A s) (Q : post A) : (s g).1 i -> (forall v m, (s g).2 (Val v) m -> valid m -> Q (Val v) m) -> (forall x m, (s g).2 (Exn x) m -> valid m -> Q (Exn x) m) -> vrf i e Q.
proof: Proof. case: e=>e /= /[apply] Hp Hv He; apply: vrfV=>V /=. by apply/vrf_post/Hp; case=>[v|ex] m Vm H; [apply: Hv | apply: He]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)