proposition: Lemma pred_sepcon_unique_sepcon1: forall (P: B -> Prop) p x0, sepcon_unique1 p -> pred_sepcon P p * p x0 |-- !! (~ P x0).
proof: Proof. intros. apply not_prop_right; intro. unfold pred_sepcon; normalize. rewrite <- H1 in H0. eapply derives_trans; [apply sepcon_derives; [apply iter_sepcon_in_true; eauto| apply derives_refl] |]. rewrite sepcon_comm, <- sepcon_assoc. eapply derives_trans; [apply sepcon_derives; [apply H | apply derives_refl] |]. normalize. 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