proposition: Lemma try_frame : frameable try_prog.
proof: Proof. move=>i j [Vi [Pi][E1 E2]] Vij [_ [Pij _]] y m [x][h][/=]. move: (fr_st Pi Vij Pij)=>H. case: x=>[x|ex] Ph. - case=>Ph'. case: (H _ _ Ph)=>h1[Eh V1 Ph1]; subst h. rewrite (pf_irr (validL Vij) Vi) in Ph1 *; move: (E1 _ _ Ph1)=>P21. rewrite (pf_irr (dstr_valid Ph) V1). case/(fr_st P21 V1 Ph')=>h2[Em Vm Ph2]. exists h2; split=>//; exists (Val x), h1, Ph1, P21. by rewrite (pf_irr (dstr_valid Ph1) (validL V1)). case=>Ph'. case: (H _ _ Ph)=>h1[Eh V1 Ph1]; subst h. rewrite (pf_irr (validL Vij) Vi) in Ph1 *; move: (E2 _ _ Ph1)=> P21. rewrite (pf_irr (dstr_valid Ph) V1). case/(fr_st P21 V1 Ph')=>h2[Em Vm Ph2]. exists h2; split=>//; exists (Exn ex), h1, Ph1, P21. by rewrite (pf_irr (dstr_valid Ph1) (validL V1)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)