proposition: Lemma valid_upath_app_2: forall g p1 p2, valid_upath g p1 -> valid_upath g p2 -> (last_error p1) = (hd_error p2) -> valid_upath g (p1++(tail p2)).
proof: Proof. intros. apply valid_upath_app. apply H. apply (valid_upath_tail g p2 H0). unfold adjacent_err. destruct (last_error p1) eqn:H2. destruct (hd_error p2) eqn:H3. assert (v = v0) by (inversion H1; reflexivity). destruct (hd_error (tl p2)) eqn: H5. assert (p2 = v0::v1::(tl (tl p2))). apply hd_error_tl_repr. split. apply H3. apply hd_error_tl_repr. split. apply H5. reflexivity. rewrite H6 in H0. destruct H0. rewrite H4. apply H0. assert (p2 = v0::(tl p2)). apply hd_error_tl_repr. split. apply H3. reflexivity. rewrite hd_error_none_nil in H5. unfold valid_upath in H0. rewrite H6 in H0; rewrite H5 in H0. rewrite H4; apply H0. inversion H1. assert (tl p2 = nil). destruct p2. reflexivity. inversion H1. rewrite H3. simpl. trivial. 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