proposition: Lemma vrf_frame i j (Q : post A) : vrf i e (fun y m => valid (m \+ j) -> Q y (m \+ j)) -> vrf (i \+ j) e Q.
proof: Proof. move=>H Vij; have Vi := validL Vij; case: (H Vi)=>Hi {}H. have Hij := sfm_st Hi Vij. exists Hij=>y m. case/(fr_st Hi Vij Hij)=>h [{m}-> Vhj P]. apply: H=>//. by rewrite (pf_irr Vi (validL Vij)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)