proposition: Lemma iter_sepcon_app_joinable: forall (p : B -> A) (l1 l2 : list B), joinable p -> (forall x, In x l1 -> ~ In x l2) -> disjointed (iter_sepcon l1 p) (iter_sepcon l2 p).
proof: Proof. intros; induction l1; simpl; auto. + apply disj_comm, disj_emp. + apply disj_comm, disj_sepcon_right. - apply disj_comm, iter_sepcon_joinable; auto. apply H0, in_eq. - apply disj_comm, IHl1. intros; apply H0, in_cons; 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