proposition: Lemma upd_Znth_twice: forall {A: Type} i (l: list A) v1 v2, 0 <= i < Zlength l -> upd_Znth i (upd_Znth i l v1) v2 = upd_Znth i l v2.
proof: Proof. intros. rewrite !upd_Znth_unfold; auto. 2: now rewrite upd_Znth_Zlength. f_equal; [|f_equal]. - rewrite sublist0_app1. + rewrite sublist_same; auto. rewrite Zlength_sublist; lia. + rewrite Zlength_sublist; lia. - assert (Zlength (sublist 0 i l) = i) by (rewrite Zlength_sublist; lia). rewrite sublist_app2; rewrite H0. 2: lia. assert (i + 1 - i = 1) by lia. rewrite H1. clear H1. rewrite Zlength_app. rewrite H0. simpl. rewrite Zlength_cons. unfold Z.succ. rewrite Zlength_sublist; [|lia..]. assert (i + (Zlength l - (i + 1) + 1) - i = Zlength l - i) by lia. rewrite H1; clear H1. rewrite sublist_1_cons. rewrite sublist_same; [auto | lia |]. rewrite Zlength_sublist; lia. Qed.
imports: CertiGraph.lib.List_ext CertiGraph.unionfind.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.ArrayGraph CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_array_graph Coq.Lists.List CertiGraph.unionfind.uf_arr_specs VST.floyd.library