proposition: Theorem ulist_def: forall l a, In a l -> ulist l -> ~ (exists l1 , permutation l (a :: (a :: l1)) ).
proof: Proof. intros l a H H0 [l1 H1]. absurd (ulist (a :: (a :: l1))); auto. intros H2; inversion_clear H2; simpl; auto with datatypes. apply ulist_perm with ( 1 := H1 ); auto. Qed.
imports: List Arith Permutation ListSet