proposition: Lemma pred_sepcon_ramif_x: forall (G L L' G': B -> Prop) (p p': B -> A), (exists Pf, Prop_join L Pf G /\ Prop_join L' Pf G' /\ (forall y, Pf y -> p y = p' y)) -> pred_sepcon G p |-- pred_sepcon L p * (pred_sepcon L' p' -* pred_sepcon G' p').
proof: Proof. intros. pose proof pred_sepcon_ramif_xQ (fun _: unit => True) G L (fun _ => L') (fun _ => G') p (fun _ => p'). rewrite allp_unit in H0. rewrite prop_imp in H0 by auto. apply H0. 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