proposition: Lemma semax_ramification_PQ: forall A Delta c G L (L' G': A -> _), G |-- L * ModBox c (allp (L' -* G')) -> semax Delta L c (normal_ret_assert (exp L')) -> semax Delta G c (normal_ret_assert (exp G')).
proof: Proof. intros. apply ramify_PQ_reduce0 in H. eapply semax_ramification_P; eauto. 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