proposition: Lemma epath_to_vpath_foot': forall (g: PreGraph V E) l v, valid_path g (v, l) -> last_error (epath_to_vpath g (v,l)) = Some (pfoot g (v,l)).
proof: Proof. unfold epath_to_vpath; induction l; intros. reflexivity. destruct l. reflexivity. rewrite pfoot_cons. 2: auto. assert (valid_path g (dst g a, e::l)). apply H. rewrite <- IHl. 2: auto. apply last_error_cons. simpl. unfold not; intros. destruct l; inversion H1. Qed.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph