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