proposition: Lemma ram_revert_exists_pre: forall {A} (x : A) Delta F P c Q, semax_ram Delta F (EX x : A, P x) c Q -> semax_ram Delta F (P x) c Q.
proof: Proof. intros. eapply semax_ram_pre; [| eauto]. apply (exp_right x); 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