proposition: Lemma gU G A (s : spec G A) g i (e : STspec G s) (Q : post A) : (s g).1 Unit -> (forall v m, (s g).2 (Val v) m -> valid (m \+ i) -> Q (Val v) (m \+ i)) -> (forall x m, (s g).2 (Exn x) m -> valid (m \+ i) -> Q (Exn x) (m \+ i)) -> vrf i e Q.
proof: Proof. case: e=>e /= /[apply] Hp Hv Hx; rewrite -(unitL i). apply/vrf_frame/vrf_post/Hp. by case=>[x|ex] n _ =>[/Hv|/Hx]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)