proposition: Lemma pred_sepcon_sepcon1: forall (P P': B -> Prop) p x0, (forall x, P' x <-> P x \/ x = x0) -> ~ P x0 -> pred_sepcon P' p = pred_sepcon P p * p x0.
proof: Proof. intros. rewrite <- pred_sepcon_sepcon with (Q := fun x => x = x0) (P := P). + f_equal. apply pred_sepcon1. + split; intros. - specialize (H a). assert (a = x0 -> ~ P a) by (intro; subst; auto). tauto. - subst. specialize (H x0). tauto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.List_ext VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.Morphisms CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize