Доказать с помощью аксиомы структурной индукции справедливость свойств

error "Индекс не может быть меньше нуля"

...
import {-# SOURCE #-} GHC.Exception( errorCallWithCallStackException )
 
-- | 'error' stops execution and displays an error message.
error :: forall (r :: RuntimeRep). forall (a :: TYPE r).
         HasCallStack => [Char] -> a
error s = raise# (errorCallWithCallStackException s ?callStack)
          -- Bleh, we should be using 'GHC.Stack.callStack' instead of
          -- '?callStack' here, but 'GHC.Stack.callStack' depends on
          -- 'GHC.Stack.popCallStack', which is partial and depends on
          -- 'error'.. Do as I say, not as I do.
 
-- | A variant of 'error' that does not produce a stack trace.
--
-- @since 4.9.0.0
errorWithoutStackTrace :: forall (r :: RuntimeRep). forall (a :: TYPE r).
                          [Char] -> a
errorWithoutStackTrace s =
  -- we don't have withFrozenCallStack yet, so we just inline the definition
  let ?callStack = freezeCallStack emptyCallStack
  in error s
...

...
-- | List index (subscript) operator, starting from 0.
-- It is an instance of the more general 'Data.List.genericIndex',
-- which takes an index of any integral type.
(!!)                    :: [a] -> Int -> a
#ifdef USE_REPORT_PRELUDE
xs     !! n | n < 0 =  errorWithoutStackTrace "Prelude.!!: negative index"
[]     !! _         =  errorWithoutStackTrace "Prelude.!!: index too large"
(x:_)  !! 0         =  x
(_:xs) !! n         =  xs !! (n-1)
#else
 
-- We don't really want the errors to inline with (!!).
-- We may want to fuss around a bit with NOINLINE, and
-- if so we should be careful not to trip up known-bottom
-- optimizations.
tooLarge :: Int -> a
tooLarge _ = errorWithoutStackTrace (prel_list_str ++ "!!: index too large")
 
negIndex :: a
negIndex = errorWithoutStackTrace $ prel_list_str ++ "!!: negative index"
 
{-# INLINABLE (!!) #-}
xs !! n
  | n < 0     = negIndex
  | otherwise = foldr (\x r k -> case k of
                                   0 -> x
                                   _ -> r (k-1)) tooLarge xs n
#endif
...

*Main> let xs=[1..3]
*Main> xs !! (-1)
*** Exception: Prelude.!!: negative index
*Main> reverse xs !! (length xs - (-1) -1)
*** Exception: Prelude.!!: index too large
*Main>