proposition: Theorem incl_length_repetition: forall (l1 l2 : list A), incl l1 l2 -> lt (length l2) (length l1) -> (exists a , exists ll1 , exists ll2 , exists ll3 , l1 = ll1 ++ ((a :: ll2) ++ (a :: ll3)) /\ ulist (ll1 ++ (a :: ll2)) ).
proof: Proof. intros l1 l2 H H0; apply ulist_inv_ulist. intros H1; absurd (le (length l1) (length l2)); auto with arith. apply ulist_incl_length; auto. Qed.
imports: List Arith Permutation ListSet