proposition: Lemma precise_exp_iter_sepcon: forall (P : B -> A) (Q: list B -> Prop), sepcon_unique1 P -> (exists x : list B, Q x /\ NoDup x) \/ ~ (exists x : list B, Q x /\ NoDup x) -> (forall l, precise (P l)) -> (forall l l', Q l -> Q l' -> NoDup l -> NoDup l' -> Permutation l l') -> precise (EX l: list B, !! (Q l) && iter_sepcon l P).
proof: Proof. intros. replace (EX l : list B, !!Q l && iter_sepcon l P) with (EX l : list B, !! (Q l /\ NoDup l) && iter_sepcon l P). 2: { f_equal. extensionality l. rewrite (add_andp _ _ (iter_sepcon_unique_nodup l H)) at 2. rewrite (andp_comm _ (!! NoDup l)), <- andp_assoc, prop_and. reflexivity. } apply precise_exp_prop_andp. 1: assumption. 1: apply precise_iter_sepcon; auto. intros l l'. specialize (H2 l l'). intros. apply iter_sepcon_permutation. 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