proposition: Lemma disj_mapsto_: forall {cs: composite_env} sh t1 t2 p1 p2, ~ pointer_range_overlap p1 (sizeof t1) p2 (sizeof t2) -> disjointed (EX v1: val, mapsto sh t1 p1 v1) (EX v2: val, mapsto sh t2 p2 v2).
proof: Proof. exact @disj_mapsto_. Qed.
imports: CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.alg_seplog CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.ramification_lemmas CertiGraph.veric_ext.seplog VST.veric.address_conflict VST.veric.SeparationLogic