proposition: Lemma frame_star i (Q : post A) (r : Pred heap) : i \In (fun h => vrf h e Q) # r -> vrf i e (fun v => Q v # r).
proof: Proof. case=>h1[h2][{i}-> H1 H2]. apply: vrf_frame=>V1; case: (H1 V1)=>Hp Hr. exists Hp=>y m Pm Vm2. exists m, h2; split=>//. by apply: Hr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)