proposition: Lemma pred_sepcon_False: forall p, pred_sepcon (fun _ => False) p = emp.
proof: Proof. intros. unfold pred_sepcon. apply pred_ext. + apply exp_left; intros. normalize. destruct x; [simpl; auto |]. specialize (H b); simpl in H; tauto. + apply (exp_right nil). normalize. simpl. apply andp_right; auto. apply prop_right; constructor. 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