proposition: Lemma neg_pure_from_pred_sepcon: forall (P Q: B -> Prop) p, (forall x, Q x -> p x |-- FF) -> pred_sepcon P p |-- !! (Disjoint _ P Q).
proof: Proof. intros. unfold pred_sepcon; normalize; intros. rename x into l. normalize. 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 <- H0 in H2. eapply derives_trans; [eapply iter_sepcon_in_true; eauto |]. eapply derives_trans; [apply sepcon_derives; [apply H; auto | 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