proposition: Lemma lgd_vertex_rep_eq_in_diff_vert: forall sh g v' v v1 e n, 0 <= n < Zlength (make_fields g v) -> Znth n (make_fields g v) = inr e -> v1 <> v -> vertex_rep sh g v1 = vertex_rep sh (labeledgraph_gen_dst g e v') v1.
proof: Proof. intros. unfold vertex_rep. rewrite lgd_vertex_address_eq, <- lgd_make_header_eq. f_equal. unfold make_fields_vals. rewrite <- lgd_raw_mark_eq. simple_if_tac; [f_equal |]; rewrite (lgd_map_f2v_diff_vert_eq _ g v v' v1 e n); try reflexivity; assumption. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List