proposition: Lemma allocb_dstrict : def_strict allocb_prog.
proof: Proof. by move=>i [] Vi y [l][]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)