proposition: Lemma valid_upath_vvalid: forall g p v, valid_upath g p -> In v p -> vvalid g v.
proof: Proof. induction p; intros. contradiction. simpl in H0. destruct H0. subst a. destruct p. auto. destruct H. destruct H. destruct H. destruct H. destruct H1; destruct H1. rewrite <- H1. apply H2. rewrite <- H3; apply H2. apply IHp. apply (valid_upath_tail' g p a H). auto. 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