proposition: Lemma valid_upath_tail': forall g p u, valid_upath g (u::p) -> valid_upath g p.
proof: Proof. induction p; intros. - simpl; auto. - simpl in H. destruct H. destruct p. + simpl; auto. + destruct H0. simpl. split. apply H0. apply 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