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