proposition: Lemma gX G A (s : spec G A) g (m : heapPCM) m0 j tm k wh r2 (e : STspec G s) (fm : Syntactify.form (empx _) j tm) (fu : uform m0 (Syntactify.untag fm)) (f : forall q, form q r2) (fg : PullX.rform j k tm wh (Some (untag (heap_of (f m0))))) (Q : post A) : untagU fu = m -> (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 (fg : heapPCM) e Q.
proof: Proof. case: e=>e /= H; case: fu=>_ ->/= Em Hp Hv Hx; rewrite -{}Em in Hp. rewrite (pullX (Syntactify.untag fm)) formE joinCA joinA. apply: vrfV=>/validL/Hp/H V. apply/vrf_frame/vrf_post/V. by case=>[v|x] 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)