proposition: Lemma fits_upath_vertex_src_In: forall g p l e, fits_upath g l p -> In e l -> In (src g e) p.
proof: Proof. induction p; intros. destruct l; auto. destruct p. destruct l; simpl in H; contradiction. destruct l. contradiction. destruct H0. subst e0. destruct H. destruct H. destruct H1. left; symmetry; apply H1. right. left. symmetry; apply H1. right. apply (IHp l). apply 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