proposition: Lemma fits_upath_vertex_in_path: forall g p e l, fits_upath g l p -> In e l -> In (src g e) p /\ In (dst g e) p.
proof: Proof. induction p; intros. destruct l; auto. destruct p. destruct l; [contradiction|auto]. simpl in H; contradiction. destruct l. simpl in H; contradiction. destruct H0. subst e0. destruct H. destruct H. destruct H1; destruct H1; subst a; subst v. split. left; auto. right; left; auto. split. right; left; auto. left; auto. assert (In (src g e) (v :: p) /\ In (dst g e) (v :: p)). apply (IHp e l). apply H. auto. destruct H1. split; right; 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