proposition: Lemma iter_sepcon_ocon (eq_dec: forall x y : B, {x = y} + {x <> y}): forall l1 l2 p, NoDup l1 -> NoDup l2 -> (forall x, precise (p x)) -> joinable p -> iter_sepcon l1 p ⊗ iter_sepcon l2 p = iter_sepcon (nodup eq_dec (l1 ++ l2)) p.
proof: Proof. intros. symmetry; apply iter_sepcon_ocon'; auto. + apply NoDup_nodup; auto. + intros. rewrite nodup_In. rewrite in_app_iff. tauto. 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