proposition: Lemma read_frame : frameable read_prog.
proof: Proof. move=>i j [Hx [v E]] Vij _ _ _ [w [-> -> H]]. exists i; split=>//; exists w; split=>{v E}//. by rewrite findUnL // Hx in H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)