proposition: Lemma pre_sup_sfmono u : safe_mono (pre_sup u).
proof: Proof. move=>i j Pi Vij e He. by apply: sfm_st=>//; apply: Pi. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)