proposition: Lemma vpp_Znth: forall (x : VType) (g : LGraph) (i : Z), 0 <= i < Zlength (raw_fields (vlabel g x)) -> Znth i (vertex_pos_pairs g x) = inr (x, i).
proof: Proof. intros. unfold vertex_pos_pairs. assert (0 <= i < Zlength (nat_inc_list (length (raw_fields (vlabel g x))))) by (rewrite Zlength_correct, nat_inc_list_length, <- Zlength_correct; assumption). rewrite Znth_map by assumption. do 2 f_equal. rewrite <- nth_Znth by assumption. rewrite nat_inc_list_nth. 1: rewrite Z2Nat.id; lia. rewrite <- ZtoNat_Zlength, <- Z2Nat.inj_lt; lia. 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