proposition: Lemma uforest'_unique_lpath: forall p l1 l2 g, uforest' g -> simple_upath g p -> fits_upath g l1 p -> fits_upath g l2 p -> l1 = l2.
proof: Proof. induction p; intros. destruct l1. destruct l2. auto. simpl in H2; contradiction. simpl in H1; contradiction. destruct p. destruct l1. destruct l2. auto. simpl in H2; contradiction. contradiction. destruct l1. contradiction. destruct l2. contradiction. destruct H1. destruct H2. assert (e = e0). destruct H. destruct H5. apply (H5 a v). split; auto. subst e0. assert (l1 = l2). apply (IHp l1 l2 g); auto. apply (simple_upath_tail g a (v::p)); auto. subst l1. 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