proposition: Lemma try_sfmono : safe_mono try_pre.
proof: Proof. move=>i j [Vi [Pi][E1 E2]] Vij. have Pij := sfm_st Pi Vij. exists Vij, Pij; split. - move=>y m. case/(fr_st Pi Vij Pij)=>h [{m}-> Vhj]. rewrite (pf_irr (validL Vij) Vi)=>/E1 Ph. by apply: sfm_st=>//; apply: (validL Vhj). move=>ex m. case/(fr_st Pi Vij Pij)=>h [{m}-> Vhj]. rewrite (pf_irr (validL Vij) Vi)=>/E2 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)