proposition: Lemma disj_address_mapsto_: forall sh l1 ch1 l2 ch2, ~ range_overlap l1 (size_chunk ch1) l2 (size_chunk ch2) -> disjointed (EX v1: val, address_mapsto ch1 v1 sh l1) (EX v2: val, address_mapsto ch2 v2 sh l2).
proof: Proof. intros. eapply disj_derives_i; [| | apply disj_VALspec_range; eauto]; apply exp_left; intro; apply address_mapsto_VALspec_range. Qed.
imports: VST.veric.base VST.veric.rmaps VST.veric.rmaps_lemmas VST.veric.compcert_rmaps VST.veric.slice VST.veric.Clight_lemmas VST.veric.tycontext VST.veric.expr VST.veric.res_predicates CertiGraph.msl_ext.precise CertiGraph.msl_ext.overlapping