proposition: Lemma upath_simplifiable_edges: forall g p l u v, connected_by_path g p u v -> fits_upath g l p -> exists p' l', connected_by_path g p' u v /\ simple_upath g p' /\ incl p' p /\ fits_upath g l' p' /\ incl l' l.
proof: Proof. induction p; intros. destruct H. destruct H1. inversion H1. destruct p. destruct H. simpl in H. simpl in H1; destruct H1. inversion H1; inversion H2. subst u; subst v. clear H1 H2. destruct l. 2: { simpl in H0; contradiction. } exists (a::nil). exists nil. split. split. simpl; auto. simpl; split; auto. split. split. simpl; auto. apply NoDup_cons. auto. apply NoDup_nil. unfold incl; intros; auto. destruct l. simpl in H0; contradiction. destruct H as [? [? ?]]. destruct H. assert (connected_by_path g (v0::p) v0 v). split. auto. split. apply hd_error_cons. rewrite last_error_cons in H2; auto. unfold not; intros. inversion H4. destruct H0. apply (IHp l v0 v H4) in H5. destruct H5 as [p' ?]. destruct H5 as [l' [? [? [? [? ?]]]]]. destruct (in_dec EV a p'). apply in_split in i. destruct i as [p1 [p2 ?]]. subst p'. exists (a::p2). apply fits_upath_split in H8. destruct H8 as [l1 [l2 [l3 [? [? ?]]]]]. exists l3. split. split. destruct H6. apply valid_upath_app_split in H6. apply H6. split. simpl in H1. simpl. apply H1. destruct H5. destruct H12. rewrite last_err_split2 in H13. auto. split. apply simple_upath_app_split in H6. apply H6. split. unfold incl; intros. destruct H12. subst a0. left; auto. right. apply H7. apply in_or_app. right. right. auto. split. auto. unfold incl; intros. right. apply H9. subst l'. apply in_or_app. right. apply in_or_app. auto. exists (a::p'). exists (e::l'). split. split. destruct p'. simpl. apply (adjacent_requires_vvalid g a v0). auto. destruct H5. destruct H10. simpl in H10. inversion H10. subst v1. split; auto. split. simpl in H1. simpl. auto. destruct H5. destruct H10. rewrite last_error_cons. auto. unfold not; intros; subst p'. inversion H10. split. split. destruct p'. simpl. apply (adjacent_requires_vvalid g a v0). auto. destruct H5. destruct H10. simpl in H10. inversion H10. subst v1. split; auto. apply NoDup_cons. auto. apply H6. split. unfold incl; intros. destruct H10. subst a0. left; auto. right; apply H7. auto. split. destruct H5. destruct H10. destruct p'. inversion H10. inversion H10. subst v1. split; auto. unfold incl; intros. destruct H10. subst a0. left. auto. right. apply H9. 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