proposition: Lemma iter_sepcon_joinable: forall (p : B -> A) (l : list B) (x : B), joinable p -> (~ In x l) -> disjointed (p x) (iter_sepcon l p).
proof: Proof. intros. induction l; simpl. + apply disj_emp. + apply disj_sepcon_right. - apply H. intro. apply H0. subst. apply in_eq. - apply IHl. intro; apply H0. apply 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