proposition: Lemma disj_sepcon_left: forall {A} {ND: NatDed A} {SL: SepLog A} {PSL: PreciseSepLog A} {OSL: OverlapSepLog A} {DSL: DisjointedSepLog A} P Q R, disjointed Q P -> disjointed R P -> disjointed (Q * R) P.
proof: Proof. intros. apply disj_comm. apply disj_comm in H. apply disj_comm in H0. apply disj_sepcon_right; auto. 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