proposition: Lemma ram_extract_exists_pre: forall A Delta F P c Q, (forall x : A, semax_ram Delta F (P x) c Q) -> semax_ram Delta F (EX x : A, P x) c Q.
proof: Proof. Opaque LiftNatDed' LiftSepLog'. induction F; intros; simpl in H |- *. Transparent LiftNatDed' LiftSepLog'. + apply extract_exists_pre; auto. + destruct a as [l g s [F0 ? ?]]. rewrite exp_sepcon1. apply IHF; 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