proposition: Lemma make_fields'_item_was_in_list: forall l v n gcptr, 0 <= n < Zlength l -> Znth n (make_fields' l v 0) = inl (inr gcptr) -> Znth n l = Some (inr gcptr).
proof: Proof. intros. rewrite <- nth_Znth; rewrite <- nth_Znth in H0; [| rewrite Zlength_correct in *..]; try rewrite make_fields'_eq_length; [|assumption..]. generalize dependent n. induction l. - intros. rewrite nth_Znth in H0; try assumption. unfold make_fields' in H0; rewrite Znth_nil in H0; inversion H0. - intro n. induction (Z.to_nat n) eqn:?. + intros. destruct a; [destruct s|]; simpl in *; try inversion H0; try reflexivity. + intros. simpl in *. clear IHn0. replace n0 with (Z.to_nat (Z.of_nat n0)) by apply Nat2Z.id. assert (0 <= Z.of_nat n0 < Zlength l). { split; try lia. destruct H; rewrite Zlength_cons in H1. apply Zsucc_lt_reg; rewrite <- Nat2Z.inj_succ. rewrite <- Heqn0; rewrite Z2Nat.id; assumption. } destruct a; [destruct s|]; simpl in H0; apply IHl; try assumption; apply make_fields'_n_doesnt_matter with (n:=1%nat); rewrite Nat2Z.id; 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