proposition: Lemma frr_Zlength: forall from to roots g roots' g', forward_roots_relation from to roots g roots' g' -> Zlength roots = Zlength roots'.
proof: Proof. induction 1; simpl; autorewrite with sublist; auto; 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