proposition: Lemma read_sfmono : safe_mono read_pre.
proof: Proof. move=>i j [Hx [v E]] Vij; split. - by rewrite domUn inE Vij Hx. by exists v; rewrite findUnL // Hx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)