fact: Definition pred_sepcon (P: B -> Prop) (p: B -> A): A := EX l: list B, !! (forall x, In x l <-> P x) && !! NoDup l && iter_sepcon l p.
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