proposition: Theorem ulist_inv_ulist: forall (l : list A), ~ ulist l -> (exists a , exists l1 , exists l2 , exists l3 , l = l1 ++ ((a :: l2) ++ (a :: l3)) /\ ulist (l1 ++ (a :: l2)) ).
proof: Proof. intros l; elim l using list_length_ind; clear l. intros l; case l; simpl; auto; clear l. intros Rec H0; case H0; auto. intros a l H H0. case (In_dec eqA_dec a l); intros H1; auto. case in_ex_app_first with ( 1 := H1 ); intros l1 [l2 [Hl1 Hl2]]; subst l. case (ulist_dec l1); intros H2. exists a; exists (@nil A); exists l1; exists l2; split; auto. simpl; apply ulist_cons; auto. case (H l1); auto. rewrite length_app; auto with arith. intros b [l3 [l4 [l5 [Hl3 Hl4]]]]; subst l1. exists b; exists (a :: l3); exists l4; exists (l5 ++ (a :: l2)); split; simpl; auto. (repeat (rewrite <- ass_app; simpl)); auto. apply ulist_cons; auto. contradict Hl2; auto. replace (l3 ++ (b :: (l4 ++ (b :: l5)))) with ((l3 ++ (b :: l4)) ++ (b :: l5)); auto with datatypes. (repeat (rewrite <- ass_app; simpl)); auto. case (H l); auto; intros a1 [l1 [l2 [l3 [Hl3 Hl4]]]]; subst l. exists a1; exists (a :: l1); exists l2; exists l3; split; auto. simpl; apply ulist_cons; auto. contradict H1. replace (l1 ++ (a1 :: (l2 ++ (a1 :: l3)))) with ((l1 ++ (a1 :: l2)) ++ (a1 :: l3)). - auto with datatypes. - (repeat (rewrite <- ass_app; simpl)); auto. Qed.
imports: List Arith Permutation ListSet