proposition: Lemma sepcon_isolate_nth: forall {A} `{INH: Inhabitant A} (P: A -> mpred) (al: list A) (i: Z), 0 <= i < Zlength al -> iter_sepcon al P = P (Znth i al) * iter_sepcon (sublist 0 i al ++ sublist (Z.succ i) (Zlength al) al) P.
proof: Proof. induction al; intros. list_solve. simpl. destruct (zeq i 0). - list_simplify. f_equal. apply iter_sepcon_permutation. subst. rewrite sublist_nil_gen by lia. simpl. rewrite sublist_pos_cons by list_solve. rewrite sublist_same by list_solve. apply Permutation_refl. - rewrite iter_sepcon_app_sepcon. list_simplify. rewrite (sublist_split 0 1 i) by list_solve. rewrite sublist_one by list_solve. list_simplify. rewrite (IHal (i-1)) by lia; clear IHal. rewrite !iter_sepcon_app_sepcon. replace (Z.succ (i-1)) with i by lia. rewrite sublist_app2 by list_solve. list_simplify. rewrite Z.sub_diag. change (Zrepeat a 1) with [a]. simpl iter_sepcon. rewrite <- !sepcon_assoc. pull_left (P a). rewrite sepcon_emp. f_equal. f_equal. list_solve. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List