proposition: Lemma ram_extract_PROP: forall Delta F (PP: Prop) (P: list Prop) QR c Post, (PP -> semax_ram Delta F (PROPx P QR) c Post) -> semax_ram Delta F (PROPx (PP :: P) QR) c Post.
proof: Proof. intros. Opaque LiftNatDed' LiftSepLog'. revert QR H; induction F; intros; simpl in H |- *. Transparent LiftNatDed' LiftSepLog'. + apply semax_extract_PROP; auto. + destruct a as [l g s [F0 ? ?]]. unfold PROPx in H |- *. rewrite sepcon_andp_prop' in H |- *. 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