proposition: Lemma Zlength_update_frames: forall frs roots, Zlength roots = Zlength (frames2rootpairs frs) -> Zlength (update_frames frs roots) = Zlength frs.
proof: Proof. induction frs; simpl; intros; auto. destruct a; simpl in *; autorewrite with sublist. f_equal. apply IHfrs; clear IHfrs. autorewrite with sublist in *. simpl in *. 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