proposition: Lemma write_mono (p1 p2 : ptr) (x1 x2 : A) : p1 = p2 -> x1 = x2 -> (write p1 x1 : ST unit) <== write p2 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)