proposition: Corollary valid_upath_concat: forall g p v, valid_upath g p -> adjacent_last g (last_error p) v -> valid_upath g (p+::v).
proof: Proof. intros. apply (valid_upath_app g p (v::nil)). apply H. simpl. destruct (last_error p); simpl in H0. apply (adjacent_requires_vvalid g v0 v H0). apply H0. destruct (last_error p); simpl in *; apply H0. 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