proposition: Lemma valid_dpath_implies_valid_upath': forall g p, valid_path' g p -> valid_upath g (epath_to_vpath' g p).
proof: Proof. intros. induction p. simpl. trivial. assert (valid_path' g p). apply (valid_path'_cons g p a H). destruct p eqn:H_p. simpl. split. exists a. split. apply H. left. split; reflexivity. apply H. assert (epath_to_vpath' g (a :: e :: l) = (src g a) :: epath_to_vpath' g (e::l)). simpl. reflexivity. rewrite H1; clear H1. apply valid_upath_cons. apply IHp. apply H0. assert (hd_error (epath_to_vpath' g (e :: l)) = Some (src g e)). destruct l; reflexivity. rewrite H1. unfold adjacent_hd. unfold adjacent. exists a. split. apply H. left. split. reflexivity. apply H. 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