proposition: Lemma lgd_map_f2v_diff_vert_eq: forall tag g v v' v1 e n, 0 <= n < Zlength (make_fields g v) -> Znth n (make_fields g v) = inr e -> v1 <> v -> map (field2val tag g) (make_fields g v1) = map (field2val tag (labeledgraph_gen_dst g e v')) (make_fields (labeledgraph_gen_dst g e v') v1).
proof: Proof. intros. rewrite lgd_make_fields_eq. apply Znth_list_eq. split. 1: repeat rewrite Zlength_map; reflexivity. intros. rewrite Zlength_map in H2. repeat rewrite Znth_map by assumption. apply lgd_f2v_eq_except_one. intro. pose proof (make_fields_edge_unique g e v v1 n j H H2 H0 H3). destruct H4. unfold not in H1. symmetry in H5. apply (H1 H5). 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