proposition: Lemma stepX G A B (s : spec G A) g (m : heapPCM) m0 j tm k wh r2 (e : STspec G s) (e2 : A -> ST B) (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 B) : untagU fu = m -> (valid m -> (s g).1 m) -> (forall v n, (s g).2 (Val v) n -> vrf (f n) (e2 v) Q) -> (forall x n, (s g).2 (Exn x) n -> valid (untag (f n)) -> Q (Exn x) (f n)) -> vrf (fg : heapPCM) (bind e e2) Q.
proof: Proof. move=>Hm Hp Hv Hx. by apply/vrf_bind/(gX _ _ Hm Hp)=>[v n H V|x n H V _]; [apply: Hv| apply: Hx]. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)