proposition: Lemma pred_sepcon_Empty: forall p, pred_sepcon (Empty_set _) p = emp.
proof: Proof. intros. rewrite <- pred_sepcon_False with p. apply pred_sepcon_proper; [| reflexivity]. intros ?. rewrite Empty_set_spec; tauto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.List_ext VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.Morphisms CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize