proposition: Lemma frames_p_update_frames_sublist: forall frs roots k, Zlength (frames2rootpairs frs) = Zlength roots -> 0 <= k <= Zlength frs -> frames_p (sublist k (Zlength frs) frs) = frames_p (sublist k (Zlength frs) (update_frames frs roots)).
proof: Proof. induction frs as [|[???]?]; intros; simpl in *; auto. autorewrite with sublist in *. simpl in *. destruct (zeq k 0). - subst k. rewrite !sublist_0_cons by list_solve. reflexivity. - rewrite !(sublist_pos_cons k) by lia. replace (Z.succ (Zlength frs) - 1) with (Zlength frs) by lia. apply IHfrs; clear IHfrs. list_solve. lia. 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