proposition: Lemma mapsto_precise: forall {Addr Val: Type} {AV: AbsAddr Addr Val} {A} {mapsto: Addr -> Val -> A} {ND: NatDed A} {SL: SepLog A} {PSL: PreciseSepLog A} {MSL: MapstoSepLog AV mapsto} p v , precise (mapsto p v).
proof: Proof. intros. eapply derives_precise; [| apply mapsto__precise]. apply (exp_right v). apply derives_refl. 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