proposition: Lemma make_fields'_edge_depends_on_index: forall n l_raw i v e, 0 <= Z.of_nat n < Zlength l_raw -> nth n (make_fields' l_raw v i) field_t_inhabitant = inr e -> e = (v, n+i)%nat.
proof: Proof. induction n as [|n' IHn']. - intros. destruct l_raw; try inversion H0. destruct r; [destruct s|]; simpl in H0; inversion H0; reflexivity. - intro. destruct l_raw; try inversion 2. replace (S n' + i)%nat with (n' + S i)%nat by lia. specialize (IHn' l_raw (S i) v e). assert (0 <= Z.of_nat n' < Zlength l_raw) by (rewrite Zlength_cons, Nat2Z.inj_succ in H; lia). assert (nth n' (make_fields' l_raw v (S i)) field_t_inhabitant = inr e) by (destruct r; [destruct s|]; simpl in H2; replace (i + 1)%nat with (S i) in H2 by lia; assumption). destruct r; [destruct s|]; simpl; apply IHn'; 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