proposition: Lemma iter_sepcon_ramif_pred_x: forall P P' (g l: list B), (exists f, Permutation g (l ++ f) /\ (forall x, In x f -> P x = P' x)) -> iter_sepcon g P |-- iter_sepcon l P * (iter_sepcon l P' -* iter_sepcon g P').
proof: Proof. intros. apply iter_sepcon_ramif_x. destruct H as [f [? ?]]; exists f. split; [| split]; intros; auto. 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