proposition: Lemma semax_ramification_Q: forall A Delta G L s (L' G': A -> _), (forall x, closed_wrt_modvars s (L' x -* G' x)) -> G |-- L * allp (L' -* G') -> semax Delta L s (normal_ret_assert (exp L')) -> semax Delta G s (normal_ret_assert (exp G')).
proof: Proof. intros. apply semax_pre_post with (P' := L * allp (L' -* G')) (R' := normal_ret_assert (exp L' * allp (L' -* G'))). + intros. apply andp_left2; auto. + intros. apply andp_left2. apply normal_ret_assert_derives'. rewrite exp_sepcon1. apply exp_left; intro x; apply (exp_right x). rewrite sepcon_comm, wand_sepcon_adjoint. apply (allp_left _ x); auto. + apply semax_frame with (F := allp (L' -* G')) in H1; [| auto with closed]. rewrite frame_normal in H1. auto. Qed.
imports: CertiGraph.lib.Equivalence_ext CertiGraph.veric_ext.SeparationLogic VST.floyd.base VST.floyd.client_lemmas VST.floyd.assert_lemmas VST.floyd.closed_lemmas VST.floyd.forward_lemmas