proposition: Lemma bind_sfmono : safe_mono bind_pre.
proof: Proof. move=>i j [Vi][Pi]P Vij. have Pij := sfm_st Pi Vij. exists Vij, Pij=>x m. case/(fr_st Pi Vij Pij)=>h [{m}-> Vhj]. rewrite (pf_irr (validL Vij) Vi)=>/P Ph. by apply: sfm_st=>//; apply: (validL Vhj). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)