proposition: Lemma pred_sepcon_prop_true: forall (P: B -> Prop) p x, P x -> pred_sepcon P p |-- p x * TT.
proof: Proof. intros. unfold pred_sepcon; normalize. intros. normalize. rename x0 into l. rewrite <- H0 in H. eapply iter_sepcon_in_true; auto. 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