proposition: Lemma valid_upath_app: forall g p1 p2, valid_upath g p1 -> valid_upath g p2 -> adjacent_err g (last_error p1) (hd_error p2) -> valid_upath g (p1++p2).
proof: Proof. induction p1; intros. - apply H0. - destruct p1. + simpl. apply valid_upath_cons. apply H0. apply adjacent_err_hd. apply H1. + rewrite <- app_comm_cons. split. apply H. apply IHp1. apply H. 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