fact: Definition allocb_prog : prog allocb_pre ptr := fun i _ _ y m => exists l, [/\ y = Val l, m = updi l (nseq n v) \+ i & valid m].
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)