proposition: Lemma bnd_is_try A B (e1 : ST A) (e2 : A -> ST B) i r : vrf i (try e1 e2 (throw B)) r -> vrf i (bind e1 e2) r.
proof: Proof. move=>H Vi; case: (H Vi)=>[[Vi'][P1 /= [E1 E2]]] {}H. have J : i \In pre_of (bind e1 e2). - exists Vi, P1=>y m. by rewrite (pf_irr Vi Vi')=>/E1. exists J=>y m /= [x][h][Ph]C. apply: H; exists x, h=>/=. rewrite (pf_irr P1 (bind_pre_proj J)) in E2 *; exists Ph. move: Ph C; case: x=>// e Ph [{y}-> {m}->]. rewrite (pf_irr Vi' Vi) in E2. by exists (E2 _ _ Ph). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)