proposition: Lemma iter_sepcon_ramif_stable_1: forall P (g: list B) (x: B), In x g -> iter_sepcon g P |-- P x * (P x -* iter_sepcon g P).
proof: Proof. intros. apply In_Permutation_cons in H. destruct H as [f ?]. apply iter_sepcon_ramif_pred_1. exists f. split; [assumption|intros; reflexivity]. Qed.
imports: CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext VST.msl.base VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize VST.msl.Coqlib2 VST.msl.ramification_lemmas