proposition: Lemma valid_path_app_cons: forall (g: EdgeLabGG) src links2u u i o, valid_path g (src, links2u) -> pfoot g (src, links2u) = u -> strong_evalid g (u,i, o) -> valid_path g (src, links2u +:: (u,i, o)).
proof: Proof. intros. apply valid_path_app. split; [assumption|]. simpl; split; trivial. destruct H1. rewrite (edge_src_fst g); simpl; assumption. Qed.
imports: Coq.ZArith.BinInt Coq.Classes.EquivDec Coq.ZArith.Zcomplements compcert.lib.Integers VST.zlist.sublist CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.FiniteGraph CertiGraph.graph.path_lemmas