proposition: Lemma iter_sepcon_ramif_pred_xQ: forall {T: Type} (Pure: T -> Prop) (P: B -> A) (P': T -> B -> A) (g l: list B), (exists f, Permutation g (l ++ f) /\ (forall a, Pure a -> forall x, In x f -> P x = (P' a) x)) -> iter_sepcon g P |-- iter_sepcon l P * (ALL a: T, !! Pure a --> (iter_sepcon l (P' a) -* iter_sepcon g (P' a))).
proof: Proof. intros. apply (iter_sepcon_ramif_xQ _ _ _ g l (fun _ => g) (fun _ => l)). 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