proposition: Lemma make_fields_edge_unique: forall g e v1 v2 n m, 0 <= n < Zlength (make_fields g v1) -> 0 <= m < Zlength (make_fields g v2) -> Znth n (make_fields g v1) = inr e -> Znth m (make_fields g v2) = inr e -> n = m /\ v1 = v2.
proof: Proof. intros. unfold make_fields in *. rewrite make_fields'_eq_Zlength in *. assert (0 <= Z.of_nat (Z.to_nat n) < Zlength (raw_fields (vlabel g v1))) by (destruct H; split; rewrite Z2Nat.id; assumption). rewrite <- nth_Znth in H1 by (rewrite make_fields'_eq_Zlength; assumption). assert (0 <= Z.of_nat (Z.to_nat m) < Zlength (raw_fields (vlabel g v2))) by (destruct H0; split; rewrite Z2Nat.id; assumption). rewrite <- nth_Znth in H2 by (rewrite make_fields'_eq_Zlength; assumption). pose proof (make_fields'_edge_depends_on_index (Z.to_nat n) (raw_fields (vlabel g v1)) 0 v1 e H3 H1). pose proof (make_fields'_edge_depends_on_index (Z.to_nat m) (raw_fields (vlabel g v2)) 0 v2 e H4 H2). rewrite H5 in H6. inversion H6. rewrite Nat.add_cancel_r, Z2Nat.inj_iff in H9 by lia. split; [assumption | reflexivity]. 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