proposition: Lemma pred_sepcon_unique_sepcon_seg: forall (P Q: B -> Prop) p, sepcon_unique1 p -> pred_sepcon P p * pred_sepcon Q p |-- !! (Disjoint _ P Q).
proof: Proof. intros. unfold pred_sepcon; normalize; intros; normalize. rename l into lQ, x into lP. eapply derives_trans with (!! (forall x, P x -> Q x -> False)). 2: apply prop_derives; rewrite Disjoint_spec; auto. rewrite prop_forall_allp. apply allp_right; intro x. rewrite !prop_impl_imp. apply imp_andp_adjoint; normalize. apply imp_andp_adjoint; normalize. rewrite <- H2 in H4. rewrite <- H0 in H5. eapply derives_trans; [apply sepcon_derives; [apply iter_sepcon_in_true; eauto| apply iter_sepcon_in_true; eauto] |]. rewrite sepcon_assoc, (sepcon_comm TT), sepcon_assoc. rewrite TT_sepcon_TT, <- 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