proposition: Lemma alloc_frame : frameable alloc_prog.
proof: Proof. move=>i j [] Vij [] _ _ [l][->-> Hl Hl2]. exists (l :-> v \+ i); rewrite -joinA; split=>//. - rewrite validUnAE validPt domPtK Hl Vij /= all_predC. apply/hasP=>[[y Hy]]; rewrite !inE=>/eqP E. by move: Hy Hl2; rewrite E=>->. exists l; split=>//. by apply/dom_NNL/Hl2. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)