proposition: Lemma gR G A (s : spec G A) g m r (e : STspec G s) (f : forall k, form k r) (Q : post A) : (valid m -> (s g).1 m) -> (forall v n, (s g).2 (Val v) n -> valid (untag (f n)) -> Q (Val v) (f n)) -> (forall x n, (s g).2 (Exn x) n -> valid (untag (f n)) -> Q (Exn x) (f n)) -> vrf (f m) e Q.
proof: Proof. case: e=>e /= H Hp Hv Hx; rewrite formE. apply: vrfV=>/validL/Hp/H V. apply/vrf_frame/vrf_post/V. by case=>[x|ex] n _ =>[/Hv|/Hx]; rewrite formE. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)