{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns -Wno-incomplete-patterns -Wno-incomplete-uni-patterns -fno-opt-coercion #-}

-- | Valid tuple size
module Debug.RecoverRTTI.Tuple.Size (
    ValidSize(..)
  , TooBig(..)
  , smallerIsValid
  , IsValidSize(..)
  , liftValidSize
  , toValidSize
  ) where

import Data.Proxy
import Data.SOP.Dict

import Debug.RecoverRTTI.Util
import Debug.RecoverRTTI.Util.TypeLevel

{-------------------------------------------------------------------------------
  Not generated
-------------------------------------------------------------------------------}

data ValidSize (n :: Nat) where
  ValidSize :: Sing n -> (forall r. TooBig n -> r) -> ValidSize n

smallerIsValid' :: forall n. ValidSize ('S n) -> ValidSize n
smallerIsValid' :: ValidSize ('S n) -> ValidSize n
smallerIsValid' = \(ValidSize (SS n) forall r. TooBig ('S n) -> r
tooBig) -> Sing n -> (forall r. TooBig n -> r) -> ValidSize n
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing n
n ((forall r. TooBig n -> r) -> ValidSize n)
-> (forall r. TooBig n -> r) -> ValidSize n
forall a b. (a -> b) -> a -> b
$ (TooBig ('S n) -> r) -> TooBig n -> r
forall r. (TooBig ('S n) -> r) -> TooBig n -> r
aux TooBig ('S n) -> r
forall r. TooBig ('S n) -> r
tooBig
  where
    aux :: (TooBig ('S n) -> r) -> TooBig n -> r
    aux :: (TooBig ('S n) -> r) -> TooBig n -> r
aux TooBig ('S n) -> r
tooBig TooBig n
TooBig = TooBig ('S n) -> r
tooBig (TooBig ('S n)
forall (n :: Nat).
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   ('S
                                                                                                                                                                                      ('S
                                                                                                                                                                                         ('S
                                                                                                                                                                                            ('S
                                                                                                                                                                                               n)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
TooBig :: TooBig ('S n))

smallerIsValid :: forall n r.
     IsValidSize ('S n)
  => Proxy ('S n)
  -> (IsValidSize n => r)
  -> r
smallerIsValid :: Proxy ('S n) -> (IsValidSize n => r) -> r
smallerIsValid Proxy ('S n)
_ IsValidSize n => r
k =
    case ValidSize n -> Dict IsValidSize n
forall (n :: Nat). ValidSize n -> Dict IsValidSize n
liftValidSize (ValidSize ('S n) -> ValidSize n
forall (n :: Nat). ValidSize ('S n) -> ValidSize n
smallerIsValid' ValidSize ('S n)
valid) of
      Dict IsValidSize n
Dict -> r
IsValidSize n => r
k
  where
    valid :: ValidSize ('S n)
    valid :: ValidSize ('S n)
valid = ValidSize ('S n)
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize

class SingI n => IsValidSize n where
  isValidSize :: ValidSize n

{-------------------------------------------------------------------------------
  Generated
-------------------------------------------------------------------------------}

data TooBig (n :: Nat) where
  TooBig :: TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

liftValidSize :: forall n. ValidSize n -> Dict IsValidSize n
liftValidSize :: ValidSize n -> Dict IsValidSize n
liftValidSize (ValidSize Sing n
n forall r. TooBig n -> r
notTooBig) = Sing n -> Dict IsValidSize n
go Sing n
n
  where
    go :: Sing n -> Dict IsValidSize n
    go :: Sing n -> Dict IsValidSize n
go Sing n
SZ =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS SZ) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS SZ)) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS SZ))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS SZ)))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS SZ))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS SZ)))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS SZ))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS _))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
        TooBig n -> Dict IsValidSize n
forall r. TooBig n -> r
notTooBig (TooBig n
forall (n :: Nat).
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    ('S
                                                                                                                       ('S
                                                                                                                          ('S
                                                                                                                             ('S
                                                                                                                                ('S
                                                                                                                                   ('S
                                                                                                                                      ('S
                                                                                                                                         ('S
                                                                                                                                            ('S
                                                                                                                                               ('S
                                                                                                                                                  ('S
                                                                                                                                                     ('S
                                                                                                                                                        ('S
                                                                                                                                                           ('S
                                                                                                                                                              ('S
                                                                                                                                                                 ('S
                                                                                                                                                                    ('S
                                                                                                                                                                       ('S
                                                                                                                                                                          ('S
                                                                                                                                                                             ('S
                                                                                                                                                                                ('S
                                                                                                                                                                                   ('S
                                                                                                                                                                                      ('S
                                                                                                                                                                                         ('S
                                                                                                                                                                                            ('S
                                                                                                                                                                                               n)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
TooBig :: TooBig n)

instance IsValidSize 'Z where
  isValidSize :: ValidSize 'Z
isValidSize = Sing 'Z -> (forall r. TooBig 'Z -> r) -> ValidSize 'Z
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing 'Z
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig 'Z -> r) -> ValidSize 'Z)
-> (forall r. TooBig 'Z -> r) -> ValidSize 'Z
forall a b. (a -> b) -> a -> b
$ TooBig 'Z -> r
forall r. TooBig 'Z -> r
\case

instance IsValidSize ('S 'Z) where
  isValidSize :: ValidSize ('S 'Z)
isValidSize = Sing ('S 'Z)
-> (forall r. TooBig ('S 'Z) -> r) -> ValidSize ('S 'Z)
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S 'Z)
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S 'Z) -> r) -> ValidSize ('S 'Z))
-> (forall r. TooBig ('S 'Z) -> r) -> ValidSize ('S 'Z)
forall a b. (a -> b) -> a -> b
$ TooBig ('S 'Z) -> r
forall r. TooBig ('S 'Z) -> r
\case

instance IsValidSize ('S ('S 'Z)) where
  isValidSize :: ValidSize ('S ('S 'Z))
isValidSize = Sing ('S ('S 'Z))
-> (forall r. TooBig ('S ('S 'Z)) -> r) -> ValidSize ('S ('S 'Z))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S 'Z))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S 'Z)) -> r) -> ValidSize ('S ('S 'Z)))
-> (forall r. TooBig ('S ('S 'Z)) -> r) -> ValidSize ('S ('S 'Z))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S 'Z)) -> r
forall r. TooBig ('S ('S 'Z)) -> r
\case

instance IsValidSize ('S ('S ('S 'Z))) where
  isValidSize :: ValidSize ('S ('S ('S 'Z)))
isValidSize = Sing ('S ('S ('S 'Z)))
-> (forall r. TooBig ('S ('S ('S 'Z))) -> r)
-> ValidSize ('S ('S ('S 'Z)))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S 'Z)))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S 'Z))) -> r)
 -> ValidSize ('S ('S ('S 'Z))))
-> (forall r. TooBig ('S ('S ('S 'Z))) -> r)
-> ValidSize ('S ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S 'Z))) -> r
forall r. TooBig ('S ('S ('S 'Z))) -> r
\case

instance IsValidSize ('S ('S ('S ('S 'Z)))) where
  isValidSize :: ValidSize ('S ('S ('S ('S 'Z))))
isValidSize = Sing ('S ('S ('S ('S 'Z))))
-> (forall r. TooBig ('S ('S ('S ('S 'Z)))) -> r)
-> ValidSize ('S ('S ('S ('S 'Z))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S 'Z))))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S ('S 'Z)))) -> r)
 -> ValidSize ('S ('S ('S ('S 'Z)))))
-> (forall r. TooBig ('S ('S ('S ('S 'Z)))) -> r)
-> ValidSize ('S ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S 'Z)))) -> r
forall r. TooBig ('S ('S ('S ('S 'Z)))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S 'Z))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S 'Z)))))
isValidSize = Sing ('S ('S ('S ('S ('S 'Z)))))
-> (forall r. TooBig ('S ('S ('S ('S ('S 'Z))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S 'Z)))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S 'Z)))))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S ('S ('S 'Z))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S 'Z))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S 'Z))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S 'Z)))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S 'Z))))) -> r
forall r. TooBig ('S ('S ('S ('S ('S 'Z))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S 'Z)))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S 'Z))))))
isValidSize = Sing ('S ('S ('S ('S ('S ('S 'Z))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S 'Z))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S 'Z))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S ('S 'Z)))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S 'Z))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r
forall r. TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S 'Z))))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
isValidSize = Sing ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r
forall r. TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
isValidSize = Sing ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r
forall r. TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
isValidSize = Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r
forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
isValidSize = Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r)
 -> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r
forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))) where
  isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
isValidSize = Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
  -> r)
 -> ValidSize
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> (forall r.
    TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> r
forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))) where
  isValidSize :: ValidSize
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
isValidSize = Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> (forall r.
    TooBig
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
  -> r)
 -> ValidSize
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> (forall r.
    TooBig
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> r
forall r.
TooBig
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))) where
  isValidSize :: ValidSize
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
isValidSize = Sing
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> (forall r.
    TooBig
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> (forall r.
    TooBig
      ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
    -> r)
-> ValidSize
     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> r
forall r.
TooBig
  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S ('S ('S ('S 'Z))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S ('S ('S 'Z)))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S ('S ('S ('S 'Z))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S ('S ('S ('S 'Z)))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S ('S ('S ('S 'Z)))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           'Z)))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S 'Z)))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S ('S ('S ('S 'Z)))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S ('S 'Z)))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           'Z))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           'Z)))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S 'Z)))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S ('S ('S ('S 'Z)))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S ('S ('S ('S 'Z)))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          'Z))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          'Z))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              'Z))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             'Z))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          'Z))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            'Z))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              'Z)))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              'Z))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             'Z))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          'Z))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          'Z))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             'Z)))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             'Z)))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 'Z)))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                'Z)))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             'Z)))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               'Z)))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 'Z))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 'Z)))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                'Z)))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             'Z)))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             'Z)))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                'Z))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                'Z))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    'Z))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   'Z))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                'Z))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  'Z))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    'Z)))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    'Z))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   'Z))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                'Z))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                'Z))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   'Z)))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   'Z)))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       'Z)))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      'Z)))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   'Z)))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     'Z)))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       'Z))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       'Z)))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      'Z)))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   'Z)))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   'Z)))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      'Z))))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      'Z))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          'Z))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         'Z))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      'Z))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     ('S
                                                                                        'Z))))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          'Z)))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          'Z))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         'Z))))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      'Z))))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      'Z))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         'Z)))))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         'Z)))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             'Z)))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            'Z)))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         'Z)))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     ('S
                                                                                        ('S
                                                                                           'Z)))))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             'Z))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             'Z)))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            'Z)))))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         'Z)))))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         'Z)))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            'Z))))))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            'Z))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                'Z))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               'Z))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            'Z))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     ('S
                                                                                        ('S
                                                                                           ('S
                                                                                              'Z))))))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                'Z)))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                'Z))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               'Z))))))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            'Z))))))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            'Z))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               'Z)))))))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               'Z)))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   'Z)))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  'Z)))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               'Z)))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     ('S
                                                                                        ('S
                                                                                           ('S
                                                                                              ('S
                                                                                                 'Z)))))))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   'Z))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   'Z)))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  'Z)))))))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               'Z)))))))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               'Z)))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  'Z))))))))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  'Z))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      'Z))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     'Z))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  'Z))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     ('S
                                                                                        ('S
                                                                                           ('S
                                                                                              ('S
                                                                                                 ('S
                                                                                                    'Z))))))))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      'Z)))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      'Z))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     'Z))))))))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  'Z))))))))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  'Z))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     'Z)))))))))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     'Z)))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         'Z)))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        'Z)))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     'Z)))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     ('S
                                                                                        ('S
                                                                                           ('S
                                                                                              ('S
                                                                                                 ('S
                                                                                                    ('S
                                                                                                       'Z)))))))))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         'Z))))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         'Z)))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        'Z)))))))))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     'Z)))))))))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     'Z)))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        'Z))))))))))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        'Z))))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            'Z))))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           'Z))))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        'Z))))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     ('S
                                                                                        ('S
                                                                                           ('S
                                                                                              ('S
                                                                                                 ('S
                                                                                                    ('S
                                                                                                       ('S
                                                                                                          'Z))))))))))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            'Z)))))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            'Z))))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           'Z))))))))))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        'Z))))))))))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        'Z))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           'Z)))))))))))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           'Z)))))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            ('S
                                                                                                               'Z)))))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              'Z)))))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           'Z)))))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     ('S
                                                                                        ('S
                                                                                           ('S
                                                                                              ('S
                                                                                                 ('S
                                                                                                    ('S
                                                                                                       ('S
                                                                                                          ('S
                                                                                                             'Z)))))))))))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            ('S
                                                                                                               'Z))))))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            ('S
                                                                                                               'Z)))))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              'Z)))))))))))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           'Z)))))))))))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           'Z)))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              'Z))))))))))))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              'Z))))))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            ('S
                                                                                                               ('S
                                                                                                                  'Z))))))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 'Z))))))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              'Z))))))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     ('S
                                                                                        ('S
                                                                                           ('S
                                                                                              ('S
                                                                                                 ('S
                                                                                                    ('S
                                                                                                       ('S
                                                                                                          ('S
                                                                                                             ('S
                                                                                                                'Z))))))))))))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            ('S
                                                                                                               ('S
                                                                                                                  'Z)))))))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            ('S
                                                                                                               ('S
                                                                                                                  'Z))))))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 'Z))))))))))))))))))))))))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              'Z))))))))))))))))))))))))))))))))))))
-> r
forall r.
TooBig
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              'Z))))))))))))))))))))))))))))))))))))
-> r
\case

instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))) where
  isValidSize :: ValidSize
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 'Z)))))))))))))))))))))))))))))))))))))
isValidSize = Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 'Z)))))))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            ('S
                                                                                                               ('S
                                                                                                                  ('S
                                                                                                                     'Z)))))))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 ('S
                                                                                                                    'Z)))))))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
  ('S
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S
                             ('S
                                ('S
                                   ('S
                                      ('S
                                         ('S
                                            ('S
                                               ('S
                                                  ('S
                                                     ('S
                                                        ('S
                                                           ('S
                                                              ('S
                                                                 ('S
                                                                    ('S
                                                                       ('S
                                                                          ('S
                                                                             ('S
                                                                                ('S
                                                                                   ('S
                                                                                      ('S
                                                                                         ('S
                                                                                            ('S
                                                                                               ('S
                                                                                                  ('S
                                                                                                     ('S
                                                                                                        ('S
                                                                                                           ('S
                                                                                                              ('S
                                                                                                                 'Z)))))))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
  TooBig
    ('S
       ('S
          ('S
             ('S
                ('S
                   ('S
                      ('S
                         ('S
                            ('S
                               ('S
                                  ('S
                                     ('S
                                        ('S
                                           ('S
                                              ('S
                                                 ('S
                                                    ('S
                                                       ('S
                                                          ('S
                                                             ('S
                                                                ('S
                                                                   ('S
                                                                      ('S
                                                                         ('S
                                                                            ('S
                                                                               ('S
                                                                                  ('S
                                                                                     ('S
                                                                                        ('S
                                                                                           ('S
                                                                                              ('S
                                                                                                 ('S
                                                                                                    ('S
                                                                                                       ('S
                                                                                                          ('S
                                                                                                             ('S
                                                                                                                ('S
                                                                                                                   'Z)))))))))))))))))))))))))))))))))))))
  -> r)
 -> ValidSize
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            ('S
                                                                                                               ('S
                                                                                                                  ('S
                                                                                                                     'Z))))))))))))))))))))))))))))))))))))))
-> (forall r.
    TooBig
      ('S
         ('S
            ('S
               ('S
                  ('S
                     ('S
                        ('S
                           ('S
                              ('S
                                 ('S
                                    ('S
                                       ('S
                                          ('S
                                             ('S
                                                ('S
                                                   ('S
                                                      ('S
                                                         ('S
                                                            ('S
                                                               ('S
                                                                  ('S
                                                                     ('S
                                                                        ('S
                                                                           ('S
                                                                              ('S
                                                                                 ('S
                                                                                    ('S
                                                                                       ('S
                                                                                          ('S
                                                                                             ('S
                                                                                                ('S
                                                                                                   ('S
                                                                                                      ('S
                                                                                                         ('S
                                                                                                            ('S
                                                                                                               ('S
                                                                                                                  ('S
                                                                                                                     'Z)))))))))))))))))))))))))))))))))))))
    -> r)
-> ValidSize
     ('S
        ('S
           ('S
              ('S
                 ('S
                    ('S
                       ('S
                          ('S