proposition: Lemma allocb_mono (x1 x2 : A) (n1 n2 : nat) : x1 = x2 -> n1 = n2 -> (allocb x1 n1 : ST ptr) <== allocb x2 n2.
proof: Proof. by move=>->->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)