proposition: Lemma Znth_list_eq {X: Type} {d: Inhabitant X}: forall (l1 l2: list X), l1 = l2 <-> (Zlength l1 = Zlength l2 /\ forall j, 0 <= j < Zlength l1 -> Znth j l1 = Znth j l2).
proof: Proof. induction l1; destruct l2; split; intros. - split; intros; reflexivity. - reflexivity. - inversion H. - destruct H. rewrite Zlength_nil, Zlength_cons in H. exfalso; rep_lia. - inversion H. - destruct H. rewrite Zlength_nil, Zlength_cons in H. exfalso; rep_lia. - inversion H. subst a. subst l1. split; intros; reflexivity. - destruct H. assert (0 <= 0 < Zlength (a :: l1)) by (rewrite Zlength_cons; rep_lia). apply H0 in H1. rewrite !Znth_0_cons in H1. subst a. rewrite !Zlength_cons in H. f_equal. rewrite IHl1. split. 1: rep_lia. intros. assert (0 < j + 1) by lia. assert (0 <= j + 1 < Zlength (x :: l1)) by (rewrite Zlength_cons; rep_lia). specialize (H0 _ H3). rewrite !Znth_pos_cons in H0 by assumption. replace (j + 1 - 1) with j in H0 by lia. assumption. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen