proposition: Lemma revert_prop_left: forall {PureF: Prop}, PureF -> forall P Q R Post, PROPx (PureF :: P) (LOCALx Q (SEPx R)) |-- Post -> PROPx P (LOCALx Q (SEPx R)) |-- Post.
proof: Proof. intros. eapply derives_trans; [| eauto]. unfold PROPx; simpl; intros; normalize. 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