{-# LANGUAGE GADTs, Rank2Types #-}
import Prelude hiding (Ordering, Eq, compare, length, (!!))

data Z = Z
data S n = S n

data LT = LT
data GT = GT
data EQ = EQ

data Ordering n m o where
  EqZ :: Ordering Z Z EQ
  EqS :: (Nat n, Nat m) => Ordering n m EQ -> Ordering (S n) (S m) EQ
  LtZ :: Nat m => S m -> Ordering Z (S m) LT
  LtS :: (Nat n, Nat m) => Ordering n m LT -> Ordering (S n) (S m) LT
  GtZ :: Nat n => S n -> Ordering (S n) Z GT
  GtS :: (Nat n, Nat m) => Ordering n m GT -> Ordering (S n) (S m) GT
data SomeOrdering n m = forall o. SomeOrdering (Ordering n m o)

data IsZero n where
  IsZero :: IsZero Z
  NotZero :: Nat n => S n -> IsZero (S n)

class Nat n where
  toInt :: n -> Int
  isZero :: n -> IsZero n
  compare :: Nat m => n -> m -> SomeOrdering n m

instance Nat Z where
  toInt _ = 0
  isZero _ = IsZero
  compare _ m =
    case isZero m of
      IsZero -> SomeOrdering EqZ
      NotZero _ -> SomeOrdering $ LtZ m
instance Nat n => Nat (S n) where
  toInt ~(S n) = 1 + toInt n
  isZero n = NotZero n
  compare ~(S n) m =
    case isZero m of
      IsZero -> SomeOrdering $ GtZ (S n)
      NotZero ~(S m') ->
        case compare n m' of
          SomeOrdering o@(LtZ _) -> SomeOrdering (LtS o)
          SomeOrdering o@(LtS _) -> SomeOrdering (LtS o)
          SomeOrdering o@(GtZ _) -> SomeOrdering (GtS o)
          SomeOrdering o@(GtS _) -> SomeOrdering (GtS o)
          SomeOrdering EqZ -> SomeOrdering (EqS EqZ)
          SomeOrdering o@(EqS _) -> SomeOrdering (EqS o)

reifyInt :: Int -> (forall n. Nat n => n -> a) -> a
reifyInt 0 k = k Z
reifyInt n k = reifyInt (n-1) $ \m -> k (S m)

data Vec n a where
  Nil :: Vec Z a
  (:::) :: Nat n => a -> Vec n a -> Vec (S n) a

toList :: Vec n a -> [a]
toList Nil = []
toList (x ::: xs) = x : toList xs

fromList :: [a] -> (forall n. Nat n => Vec n a -> b) -> b
fromList [] k = k Nil
fromList (x:xs) k = fromList xs $ \xs' -> k (x ::: xs')

length :: Vec n a -> n
length Nil = Z
length (_ ::: xs) = S (length xs)

(!!) :: (Nat n, Nat m) => Vec m a -> Ordering n m LT -> a
(x ::: _) !! (LtZ _) = x
(_ ::: xs) !! (LtS o) = xs !! o
_ !! _ = error "should not happen!"

main :: IO ()
main = do
  xs <- readLn :: IO [Int]
  x <- readLn :: IO Int
  reifyInt x $ \n -> fromList xs $ \ls ->
    case compare n (length ls) of
      SomeOrdering o@(LtZ _) -> print $ ls !! o
      SomeOrdering o@(LtS _) -> print $ ls !! o
      _ -> putStrLn "out of range!"