proposition: Lemma exp_data_at_precise: forall sh t p, precise (EX v: reptype t, data_at sh t v p).
proof: Proof. intros. apply derives_precise with (memory_block sh (sizeof t) p). + apply exp_left; intro v. apply data_at_memory_block; auto. + apply seplog.memory_block_precise. Qed.
imports: VST.floyd.base VST.floyd.client_lemmas VST.floyd.assert_lemmas VST.floyd.type_induction VST.floyd.nested_pred_lemmas VST.floyd.nested_field_lemmas VST.floyd.reptype_lemmas VST.floyd.field_at CertiGraph.veric_ext.seplog CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.MapstoSL