proposition: Lemma progressive_list_repeat: forall n, list_repeat n (Vundef, Vundef) = progressive_list O n.
proof: Proof. induction n; unfold progressive_list; simpl; auto. unfold progressive_list in IHn. rewrite <- IHn. change ((Vundef, Vundef) :: list_repeat n (Vundef, Vundef)) with (((Vundef, Vundef) :: nil) ++ list_repeat n (Vundef, Vundef)). change ((Vundef, Vundef) :: nil) with (list_repeat 1 (Vundef, Vundef)). rewrite !list_repeat_app. rewrite Nat.add_comm. auto. Qed.
imports: CertiGraph.lib.List_ext CertiGraph.sample_mark.env_unionfind_arr CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.graph.UnionFind CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.ArrayGraph CertiGraph.floyd_ext.share CertiGraph.sample_mark.spatial_array_graph Coq.Lists.List