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