proposition: Lemma mapsto_unique: forall x a b w, ~ (mapsto x a * mapsto x b)%pred w.
proof: Proof. repeat intro. destruct_sepcon H h. destruct H0 as [? [? ?]]. destruct H1 as [? [? ?]]. destruct h1 as [f1 m1]. destruct h2 as [f2 m2]. destruct w as [fw mw]. hnf in *. simpl in *. specialize (H x). rewrite H3 in *. rewrite H5 in *. inversion H. inversion H9. Qed.
imports: VST.msl.msl_direct FunctionalExtensionality CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.overlapping_direct CertiGraph.heap_model_direct.SeparationAlgebra Peano_dec