proposition: Lemma mapsto_conflict: forall p1 p2 v1 v2, p1 = p2 -> mapsto p1 v1 * mapsto p2 v2 |-- FF.
proof: Proof. intros. subst. intro w. apply mapsto_unique. Qed.
imports: VST.msl.msl_direct FunctionalExtensionality CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.overlapping_direct CertiGraph.heap_model_direct.SeparationAlgebra Peano_dec