proposition: Lemma disj_prop_andp_left: forall {A} {ND: NatDed A} {SL: SepLog A} {PSL: PreciseSepLog A} {OSL: OverlapSepLog A} {DSL: DisjointedSepLog A} (P: Prop) Q R, ({P} + {~ P}) -> (P -> disjointed Q R) -> disjointed ((!! P) && Q) R.
proof: Proof. intros. destruct H. + apply H0 in p. eapply disj_derives; [ | | exact p]. - apply andp_left2, derives_refl. - apply derives_refl. + eapply disj_derives; [ | | apply FF_disj]. - apply andp_left1. normalize. - apply derives_refl. Qed.
imports: VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List CertiGraph.msl_ext.seplog CertiGraph.msl_ext.abs_addr