proposition: Lemma dealloc_dstrict : def_strict dealloc_prog.
proof: Proof. move=>i _ Vi _ [_ E _]. suff {E}: valid (free i x) by rewrite -E. by rewrite validF. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)