proposition: Lemma stepE G A B (s : spec G A) g i (e : STspec G s) (e2 : A -> ST B) (Q : post B) : (s g).1 i -> (forall x m, (s g).2 (Val x) m -> vrf m (e2 x) Q) -> (forall x m, (s g).2 (Exn x) m -> valid m -> Q (Exn x) m) -> vrf i (bind e e2) Q.
proof: Proof. move=>Hp Hv He. by apply/vrf_bind/(gE _ Hp)=>[v m P|x m P _] V; [apply: Hv | apply: He]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)