proposition: Lemma pred_sepcon_sepcon: forall (P Q R: B -> Prop) p, Prop_join P Q R -> pred_sepcon P p * pred_sepcon Q p = pred_sepcon R p.
proof: Proof. intros. destruct H. unfold pred_sepcon; apply pred_ext. + rewrite exp_sepcon1. apply exp_left; intro lP. rewrite exp_sepcon2. apply exp_left; intro lQ. normalize. apply (exp_right (lP ++ lQ)). apply andp_right; [apply andp_right |]. - apply prop_right. intros. rewrite in_app_iff. firstorder. - apply prop_right. apply NoDup_app_inv; auto. firstorder. - rewrite <- iter_sepcon_app_sepcon; auto. + apply exp_left; intro l. rewrite andp_assoc. do 2 (apply derives_extract_prop; intro). destruct (spec_list_split l P Q R H2 H1 (conj H H0)) as [lp [lq [? [? [? [? ?]]]]]]. rewrite exp_sepcon1. apply (exp_right lp). rewrite exp_sepcon2. apply (exp_right lq). normalize. rewrite H7, iter_sepcon_app_sepcon; auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.List_ext VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.Morphisms CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize