proposition: Theorem nth_ulist: forall a i j (l: list A), i < length l -> j < length l -> ulist l -> nth i l a = nth j l a -> i = j.
proof: Proof. intros a i j l; generalize i j; elim l; simpl; clear l i j. intros i j H; contradict H; auto with arith. intros b l1 Rec i j; case i; case j; auto with arith; clear i j. intros j _ H1 H2 H3; absurd (In b l1); auto. inversion H2; auto. subst; apply nth_In; auto with arith. intros i H1 _ H2 H3; absurd (In b l1); auto. inversion H2; auto. subst; apply nth_In; auto with arith. intros j i H1 H2 H3 H4; inversion H3; auto with arith. Qed.
imports: List Arith Permutation ListSet