proposition: Lemma pred_sepcon_ramif_xQ: forall {T: Type} (Pure: T -> Prop) (G L: B -> Prop) (L' G': T -> B -> Prop) (p: B -> A) (p': T -> B -> A), (exists Pf, Prop_join L Pf G /\ (forall a, Pure a -> Prop_join (L' a) Pf (G' a)) /\ (forall a, Pure a -> (forall y, Pf y -> p y = (p' a) y))) -> pred_sepcon G p |-- pred_sepcon L p * (ALL a: T, !! Pure a --> (pred_sepcon (L' a) (p' a) -* pred_sepcon (G' a) (p' a))).
proof: Proof. intros. destruct H as [Pf [? [? ?]]]. RAMIF_Q'.formalize. apply RAMIF_Q'.solve with (pred_sepcon Pf p). + simpl; auto. + apply derives_refl'; symmetry. apply pred_sepcon_sepcon; auto. + intros. normalize. specialize (H0 _ H2). specialize (H1 _ H2). apply derives_refl'. rewrite (pred_sepcon_strong_proper Pf Pf p (p' x)) by (auto; intros; tauto). rewrite sepcon_comm; apply pred_sepcon_sepcon; 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