proposition: Lemma alloc_dstrict : def_strict alloc_prog.
proof: Proof. move=>i [] Vi _ [l][_ E Hl Hl2]. suff {E}: valid (l :-> v \+ i) by rewrite -E. by rewrite validPtUn; apply/and3P. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)