fact: Definition dealloc_prog : prog dealloc_pre unit := fun i _ _ y m => [/\ y = Val tt, m = free i x & x \in dom i].
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)