proposition: Lemma mapsto_inj: forall p v1 v2, mapsto p v1 && mapsto p v2 |-- !! (v1 = v2).
proof: Proof. intros; simpl; intro w; intros. destruct H. destruct H as [? [? ?]]. destruct H0 as [? [? ?]]. rewrite H2 in H4. inversion H4. subst; auto. Qed.
imports: VST.msl.msl_direct FunctionalExtensionality CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.overlapping_direct CertiGraph.heap_model_direct.SeparationAlgebra Peano_dec