proposition: Lemma dealloc_frame : frameable dealloc_prog.
proof: Proof. move=>i j Hx Vij Hx' _ _ [->-> _]. exists (free i x); split=>//; rewrite /dealloc_pre -!toPredE /= in Hx Hx'. - by apply/freeUnR/dom_inNL/Hx. by apply: validFUn. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)