proposition: Lemma lst_reachable_unique: forall v1 p1 v2 p2 x r1 r2 P, g |= (v1, p1) is x ~o~> r1 satisfying P -> g |= (v2, p2) is x ~o~> r2 satisfying P -> length p1 <= length p2 -> exists p3, p2 = p1 ++ p3 /\ g |= (r1, p3) is r1 ~o~> r2 satisfying P.
proof: Proof. intros. destruct H as [[? ?] ?]. destruct H0 as [[? ?] ?]. simpl in H, H0. subst v1 v2. pose proof H3. pose proof H5. destruct H as [? _]. destruct H0 as [? _]. destruct (lst_valid_path_unique _ _ _ H H0 H1) as [p3 ?]. clear H H0. exists p3. split; auto. split; [split |]. - simpl. auto. - destruct p3. + rewrite app_nil_r in H6. subst p2. simpl. rewrite H2 in H4. auto. + rewrite H6 in H4. rewrite pfoot_app_cons with (v2 := r1) in H4. auto. - subst p2. apply good_path_app in H5. destruct H5 as [_ ?]. rewrite H2 in H. auto. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph