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