proposition: Lemma semax_ram_unlocalize': forall Delta l g s F P c Q P' Frame (frame_sound: g |-- l * ModBox (Ssequence s Sskip) Frame), Frame |-- P -* P' -> semax_ram Delta F P' c Q -> semax_ram Delta (RAM_FRAME.Build_SingleFrame l g s (RAM_FRAME.Build_SingleFrame' Frame Sskip frame_sound) :: F) P c Q.
proof: Proof. intros. Opaque LiftNatDed' LiftSepLog'. simpl. Transparent LiftNatDed' LiftSepLog'. eapply semax_ram_pre; [| eauto]. rewrite sepcon_comm. apply wand_sepcon_adjoint. eapply derives_trans; [| apply H]. apply EnvironBox_T; apply vars_relation_Equivalence. Qed.
imports: CertiGraph.lib.Ensembles_ext CertiGraph.lib.Relation_ext CertiGraph.lib.List_ext CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.ramification VST.floyd.base VST.floyd.canon VST.floyd.assert_lemmas VST.floyd.client_lemmas VST.floyd.closed_lemmas