proposition: Lemma vrf_bind i (Q : post B) : vrf i e1 (fun x m => match x with | Val x' => vrf m (e2 x') Q | Exn e => valid m -> Q (Exn e) m end) -> vrf i bind Q.
proof: Proof. move=>H Vi; case: (H Vi)=>Hi {}H /=. have Hi' : i \In bind_pre. - by exists Vi, Hi=>x m Pm; case: (H _ _ Pm (dstr_valid Pm)). exists Hi'=>y j /= [x][m][Pm] C. rewrite (pf_irr Hi (bind_pre_proj Hi')) in H. case: x Pm C=>[x|e] Pm; move: (H _ _ Pm (dstr_valid Pm))=>{}H. - by case=>Pm2 Pj; case: H=>Pm2'; apply; rewrite (pf_irr Pm2' Pm2). by case=>->->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)