proposition: Lemma gepl_value: forall (e: EType) k (g1 g2: LGraph) vpl, In e (get_edges g2 (fst e)) -> In (k, fst e) vpl -> vlabel g1 k = vlabel g2 (fst e) -> In (k, snd e, e) (gen_edge_pair_list g1 vpl).
proof: Proof. intros. induction vpl; [inversion H0|]. unfold gen_edge_pair_list. simpl. fold (gen_edge_pair_list g1 vpl). simpl in H0. rewrite in_app_iff. now destruct H0; [left; subst a; eapply gsepl_value; eauto| right; apply IHvpl]. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics 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 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph