proposition: Lemma valid_path_valid: forall (g : Gph) p n, valid_path g p -> In_path g n p -> vvalid g n.
proof: Proof. intros g p. destruct p as [v p]. revert v. induction p; intros. + simpl in *. hnf in H0. simpl in H0. destruct H0. 1: subst; auto. destruct H0 as [e [? _]]. inversion H0. + rewrite in_path_or_cons in H0. 2: destruct H; auto. destruct H0. - subst. destruct H. subst. simpl in H0. destruct p; [|destruct H0 as [H0 _]]; destruct H0 as [_ [? _]]; auto. - apply valid_path_cons in H. apply (IHp (dst g a)); auto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec