proposition: Lemma Subpath_trans: forall g p1 p2 p3, Subpath g p1 p2 -> Subpath g p2 p3 -> Subpath g p1 p3.
proof: Proof. intros. destruct p1 as [v1 p1]. destruct p2 as [v2 p2]. destruct p3 as [v3 p3]. destruct H, H0. split; unfold fst, snd in *. 1: apply incl_tran with p2; auto. destruct H1, H2. + subst v1 v2. left; auto. + subst. right; auto. + subst. destruct H1 as [e [? ?]]. right. exists e. split; auto. + destruct H1 as [e [? ?]]. right. exists e. split; 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