proposition: Lemma path_nodup_length : eq_midex A -> forall y l x, path x y l -> exists l', ~In x l' /\ ~In y l' /\ nodup l' /\ length l'<= length l /\ l' [= l /\ path x y l'.
proof: Proof. induction l; intros; simpl in H0. exists (nil : list A). simpl. pose (incl_nil (nil : list A)). pose (Nat.le_0_l 0). tauto. destruct (IHl a). tauto. destruct (H y a). exists (nil : list A). simpl. pose (Nat.le_0_l (S (length l))). pose (incl_nil (a::l)). rewrite H2. tauto. destruct (In_midex H x x0). destruct (In_elim_right H x x0). hyp. destruct H4. exists x2. split. tauto. split. intro. absurd (In y x0). tauto. rewrite (proj1 H4). apply in_or_app. simpl. tauto. rewrite (proj1 H4) in H1. split. destruct (nodup_app_elim_right x1 (x::x2)). tauto. tauto. split. rewrite (length_app x1 (x::x2)) in H1. simpl in H1|-* . lia. split. trans (x::x2). apply incl_tl. refl. trans (x1++(x::x2)). apply incl_appr. refl. trans l. tauto. apply incl_tl. refl. apply path_app_elim_right with x1 a. tauto. destruct (H x a). exists x0. rewrite H4. simpl. assert (length x0 <= S (length l)). lia. assert (x0 [= a :: l). apply incl_tl. tauto. tauto. exists (a::x0). simpl. assert (S (length x0) <= S (length l)). lia. assert (a :: x0 [= a :: l). apply cons_incl. refl. tauto. assert (a<>x). intro. rewrite H7 in H4. tauto. assert (a<>y). intro. rewrite H8 in H2. tauto. tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)