proposition: Theorem jump_too_far: forall i l, length l <= i -> jump i l = nil.
proof: Proof. intros i l; generalize i; elim l; simpl; auto; clear i l. intros; apply jump_nil. intros a l Rec i; case i; simpl; auto with arith. intros H; contradict H; auto with arith. Qed.
imports: List ListAux UList OrderedList