proposition: Lemma bind_frame : frameable bind_prog.
proof: Proof. move=>i j [Vi][Pi P] Vij [_ [Pij _]] y m [x][h][/=]. move: (fr_st Pi Vij Pij)=>H. case: x=>[x|e] Ph. - case=>Ph'. case: (H _ _ Ph)=>h1[Eh V1 Ph1]; subst h. rewrite (pf_irr (validL Vij) Vi) in Ph1 *; move: (P _ _ 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=>->->. case/H: Ph=>h1[Eh Vh Ph1]. by exists h1; split=>//; exists (Exn e), h1, Ph1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)