proposition: Lemma iter_sepcon_pointwise_eq: forall (l1 l2: list B) (P Q: B -> A) (x y: B), length l1 = length l2 -> (forall i, i < length l1 -> P (nth i l1 x) = Q (nth i l2 y)) -> iter_sepcon l1 P = iter_sepcon l2 Q.
proof: Proof. induction l1; intros. - destruct l2. 2: simpl in H; inversion H. simpl. reflexivity. - destruct l2. 1: simpl in H; inversion H. simpl. f_equal. + specialize (H0 O). simpl in H0. apply H0. apply NPeano.Nat.lt_0_succ. + simpl in H. apply (IHl1 _ _ _ x y); eauto. intros. specialize (H0 (S i)). simpl in H0. apply H0. apply Lt.lt_n_S. assumption. 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