proposition: Lemma allocb_frame : frameable allocb_prog.
proof: Proof. move=>i j [] Vij [] _ _ [l][->-> V]. exists (updi l (nseq n v) \+ i); rewrite -joinA; split=>//. exists l; split=>//. by rewrite joinA in V; apply: (validL V). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)