proposition: Lemma vrf_try i (Q : post B) : vrf i e (fun x m => match x with | Val x' => vrf m (e1 x') Q | Exn ex => vrf m (e2 ex) Q end) -> vrf i try Q.
proof: Proof. move=>H Vi; case: (H Vi)=>pf {}H /=. have J : i \In try_pre. - by exists Vi, pf; split=>x m Pm; case: (H _ _ Pm (dstr_valid Pm)). exists J=>y j /= [x][m][Pm]F. rewrite (pf_irr pf (try_pre_proj J)) in H. case: x Pm F=>[x|ex] Pm [Hm Hj]; case: (H _ _ Pm (dstr_valid Pm))=>pf''; apply; by rewrite (pf_irr pf'' Hm). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)