proposition: Lemma iter_sepcon_ramif_1Q: forall {T: Type} (Pure: T -> Prop) (P: B -> A) (P': T -> B -> A) (g: list B) (g': T -> list B) (x: B) (x': T -> B), (exists f, Permutation g (x :: f) /\ (forall a, Pure a -> Permutation (g' a) (x' a :: 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' a) -* iter_sepcon (g' a) (P' a))).
proof: Proof. intros. destruct H as [f [? [? ?]]]. RAMIF_Q'.formalize. apply RAMIF_Q'.solve with (iter_sepcon f P). + simpl; auto. + rewrite H; simpl; auto. + intros a; normalize. specialize (H0 _ H2). specialize (H1 _ H2). rewrite H0. rewrite sepcon_comm. apply derives_refl'; simpl; f_equal. apply iter_sepcon_func_strong; 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