proposition: Lemma frames_p_isptr: forall sh frs, frames_shell_rep sh frs |-- !! forall k, 0 <= k < Zlength frs -> isptr (frames_p (sublist k (Zlength frs) frs)).
proof: Proof. induction frs; simpl; intros. apply prop_right; list_solve. sep_apply IHfrs. Intros. rewrite prop_forall. apply allp_right. intro k. rewrite prop_forall. apply allp_right. intro. destruct (zeq k 0). subst. autorewrite with sublist. destruct a; simpl. Intros. entailer!. rewrite sublist_pos_cons by lia. sep_apply IHfrs. rewrite sepcon_andp_prop'. apply derives_extract_prop; intro. apply prop_right. autorewrite with sublist. replace (Z.succ (Zlength frs) - 1) with (Zlength frs) by lia. apply H0. list_solve. Qed.
imports: VST.veric.rmaps CertiGraph.lib.List_ext CertiGraph.graph.graph_model Coq.Program.Basics CertiGraph.graph.graph_gen CertiGraph.CertiGC.GCGraph VST.msl.wand_frame CertiGraph.CertiGC.env_graph_gc CertiGraph.CertiGC.spatial_gcgraph CertiGraph.msl_ext.iter_sepcon CertiGraph.CertiGC.gc_spec CertiGraph.msl_ext.ramification_lemmas CertiGraph.CertiGC.forward_lemmas