proposition: Lemma valid_upath_app_split: forall g p p', valid_upath g (p++p') -> (valid_upath g p /\ valid_upath g p').
proof: Proof. induction p; intros. simpl in H. split. simpl. auto. apply H. destruct p. destruct p'. simpl in *. split; auto. simpl in H. destruct H. destruct H. destruct H. split. simpl. destruct H. destruct H1; destruct H1. rewrite <- H1. apply H2. rewrite <- H3. apply H2. apply H0. destruct H. apply IHp in H0. split. split. apply H. apply H0. 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