proposition: Lemma pred_sepcon_ramif_pred_1Q: forall {T: Type} (Pure: T -> Prop) (P: B -> Prop) (p: B -> A) (p': T -> B -> A) (x: B), (exists Pf, Prop_join (eq x) Pf P /\ (forall a, Pure a -> (forall y, Pf y -> p y = (p' a) y))) -> pred_sepcon P p |-- p x * (ALL a: T, !! Pure a --> ((p' a) x -* pred_sepcon P (p' a))).
proof: Proof. intros. apply pred_sepcon_ramif_1Q. destruct H as [f [? ?]]; exists f. split; [| split]; 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