proposition: Lemma iter_sepcon_unique_nodup: forall (p : B -> A) (l : list B), sepcon_unique1 p -> iter_sepcon l p |-- !!(NoDup l).
proof: Proof. intros. induction l. + apply prop_right. constructor. + simpl. assert (p a * iter_sepcon l p |-- !!(~ In a l)). { apply not_prop_right. intros. apply (iter_sepcon_in_true p) in H0. apply derives_trans with (p a * p a * TT). + rewrite sepcon_assoc. apply sepcon_derives. apply derives_refl. auto. + specialize (H a). apply derives_trans with (FF * TT). apply sepcon_derives; auto. rewrite sepcon_comm, sepcon_FF. apply derives_refl. } apply derives_trans with (!!(NoDup l) && !!(~ In a l)). - apply andp_right; auto. apply sepcon_left2_corable_right; auto with norm. - normalize. constructor; 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