proposition: Lemma address_mapsto__precise: forall ch sh l, precise (EX v: val, address_mapsto ch v sh l).
proof: Proof. intros. eapply derives_precise. + apply exp_left; intro v. apply address_mapsto_VALspec_range. + apply VALspec_range_precise. 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