proposition: Lemma semax_ram_pre: forall Delta F P P' c Q, P' |-- P -> semax_ram Delta F P c Q -> semax_ram Delta F P' c Q.
proof: Proof. intros. Opaque LiftNatDed' LiftSepLog'. revert P P' H0 H; induction F; intros; simpl in H0 |- *. Transparent LiftNatDed' LiftSepLog'. + eapply semax_pre0; eauto. + destruct a as [l g s [F0 cont ?]]. eapply IHF; eauto. apply sepcon_derives; auto. 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