Singletons/LetStatements.hs:0:0: Splicing declarations
    singletons
      [d| foo1 :: Nat -> Nat
          foo1 x
            = let
                y :: Nat
                y = Succ Zero
              in y
          foo2 :: Nat
          foo2
            = let
                y = Succ Zero
                z = Succ y
              in z
          foo3 :: Nat -> Nat
          foo3 x
            = let
                y :: Nat
                y = Succ x
              in y
          foo4 :: Nat -> Nat
          foo4 x
            = let
                f :: Nat -> Nat
                f y = Succ y
              in f x
          foo5 :: Nat -> Nat
          foo5 x
            = let
                f :: Nat -> Nat
                f y
                  = let
                      z :: Nat
                      z = Succ y
                    in Succ z
              in f x
          foo6 :: Nat -> Nat
          foo6 x
            = let
                f :: Nat -> Nat
                f y = Succ y in
              let
                z :: Nat
                z = f x
              in z
          foo7 :: Nat -> Nat
          foo7 x
            = let
                x :: Nat
                x = Zero
              in x
          foo8 :: Nat -> Nat
          foo8 x
            = let
                z :: Nat
                z = (\ x -> x) Zero
              in z
          foo9 :: Nat -> Nat
          foo9 x
            = let
                z :: Nat -> Nat
                z = (\ x -> x)
              in z x
          foo10 :: Nat -> Nat
          foo10 x
            = let
                (+) :: Nat -> Nat -> Nat
                Zero + m = m
                (Succ n) + m = Succ (n + m)
              in (Succ Zero) + x
          foo11 :: Nat -> Nat
          foo11 x
            = let
                (+) :: Nat -> Nat -> Nat
                Zero + m = m
                (Succ n) + m = Succ (n + m)
                z :: Nat
                z = x
              in (Succ Zero) + z
          foo12 :: Nat -> Nat
          foo12 x
            = let
                (+) :: Nat -> Nat -> Nat
                Zero + m = m
                (Succ n) + m = Succ (n + x)
              in x + (Succ (Succ Zero))
          foo13 :: forall a. a -> a
          foo13 x
            = let
                bar :: a
                bar = x
              in foo13_ bar
          foo13_ :: a -> a
          foo13_ y = y
          foo14 :: Nat -> (Nat, Nat)
          foo14 x = let (y, z) = (Succ x, x) in (z, y) |]
  ======>
    Singletons/LetStatements.hs:(0,0)-(0,0)
    foo1 :: Nat -> Nat
    foo1 x
      = let
          y :: Nat
          y = Succ Zero
        in y
    foo2 :: Nat
    foo2
      = let
          y = Succ Zero
          z = Succ y
        in z
    foo3 :: Nat -> Nat
    foo3 x
      = let
          y :: Nat
          y = Succ x
        in y
    foo4 :: Nat -> Nat
    foo4 x
      = let
          f :: Nat -> Nat
          f y = Succ y
        in f x
    foo5 :: Nat -> Nat
    foo5 x
      = let
          f :: Nat -> Nat
          f y
            = let
                z :: Nat
                z = Succ y
              in Succ z
        in f x
    foo6 :: Nat -> Nat
    foo6 x
      = let
          f :: Nat -> Nat
          f y = Succ y in
        let
          z :: Nat
          z = f x
        in z
    foo7 :: Nat -> Nat
    foo7 x
      = let
          x :: Nat
          x = Zero
        in x
    foo8 :: Nat -> Nat
    foo8 x
      = let
          z :: Nat
          z = \ x -> x Zero
        in z
    foo9 :: Nat -> Nat
    foo9 x
      = let
          z :: Nat -> Nat
          z = \ x -> x
        in z x
    foo10 :: Nat -> Nat
    foo10 x
      = let
          (+) :: Nat -> Nat -> Nat
          (+) Zero m = m
          (+) (Succ n) m = Succ (n + m)
        in ((Succ Zero) + x)
    foo11 :: Nat -> Nat
    foo11 x
      = let
          (+) :: Nat -> Nat -> Nat
          z :: Nat
          (+) Zero m = m
          (+) (Succ n) m = Succ (n + m)
          z = x
        in ((Succ Zero) + z)
    foo12 :: Nat -> Nat
    foo12 x
      = let
          (+) :: Nat -> Nat -> Nat
          (+) Zero m = m
          (+) (Succ n) m = Succ (n + x)
        in (x + (Succ (Succ Zero)))
    foo13 :: forall a. a -> a
    foo13 x
      = let
          bar :: a
          bar = x
        in foo13_ bar
    foo13_ :: forall a. a -> a
    foo13_ y = y
    foo14 :: Nat -> (Nat, Nat)
    foo14 x = let (y, z) = (Succ x, x) in (z, y)
    type family Case_0123456789 x t where
      Case_0123456789 x '(y_0123456789, z) = y_0123456789
    type family Case_0123456789 x t where
      Case_0123456789 x '(z, y_0123456789) = y_0123456789
    type Let0123456789YSym1 t = Let0123456789Y t
    instance SuppressUnusedWarnings Let0123456789YSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789YSym0KindInference GHC.Tuple.())
    data Let0123456789YSym0 l
      = forall arg. KindOf (Apply Let0123456789YSym0 arg) ~ KindOf (Let0123456789YSym1 arg) =>
        Let0123456789YSym0KindInference
    type instance Apply Let0123456789YSym0 l = Let0123456789YSym1 l
    type Let0123456789ZSym1 t = Let0123456789Z t
    instance SuppressUnusedWarnings Let0123456789ZSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
    data Let0123456789ZSym0 l
      = forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
        Let0123456789ZSym0KindInference
    type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
    type Let0123456789X_0123456789Sym1 t = Let0123456789X_0123456789 t
    instance SuppressUnusedWarnings Let0123456789X_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,)
               Let0123456789X_0123456789Sym0KindInference GHC.Tuple.())
    data Let0123456789X_0123456789Sym0 l
      = forall arg. KindOf (Apply Let0123456789X_0123456789Sym0 arg) ~ KindOf (Let0123456789X_0123456789Sym1 arg) =>
        Let0123456789X_0123456789Sym0KindInference
    type instance Apply Let0123456789X_0123456789Sym0 l = Let0123456789X_0123456789Sym1 l
    type Let0123456789Y x =
        Case_0123456789 x (Let0123456789X_0123456789Sym1 x)
    type Let0123456789Z x =
        Case_0123456789 x (Let0123456789X_0123456789Sym1 x)
    type Let0123456789X_0123456789 x =
        Apply (Apply Tuple2Sym0 (Apply SuccSym0 x)) x
    type Let0123456789BarSym1 t = Let0123456789Bar t
    instance SuppressUnusedWarnings Let0123456789BarSym0 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Let0123456789BarSym0KindInference GHC.Tuple.())
    data Let0123456789BarSym0 l
      = forall arg. KindOf (Apply Let0123456789BarSym0 arg) ~ KindOf (Let0123456789BarSym1 arg) =>
        Let0123456789BarSym0KindInference
    type instance Apply Let0123456789BarSym0 l = Let0123456789BarSym1 l
    type Let0123456789Bar x = (x :: a)
    type (:<<<%%%%%%%%%%:+$$$$) t (t :: Nat) (t :: Nat) =
        (:<<<%%%%%%%%%%:+) t t t
    instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$$###) GHC.Tuple.())
    data (:<<<%%%%%%%%%%:+$$$) l (l :: Nat) (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$$) l l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$$) l l arg) =>
        (:<<<%%%%%%%%%%:+$$$###)
    type instance Apply ((:<<<%%%%%%%%%%:+$$$) l l) l = (:<<<%%%%%%%%%%:+$$$$) l l l
    instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$###) GHC.Tuple.())
    data (:<<<%%%%%%%%%%:+$$) l (l :: TyFun Nat (TyFun Nat Nat -> *))
      = forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$) l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$) l arg) =>
        (:<<<%%%%%%%%%%:+$$###)
    type instance Apply ((:<<<%%%%%%%%%%:+$$) l) l = (:<<<%%%%%%%%%%:+$$$) l l
    instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$###) GHC.Tuple.())
    data (:<<<%%%%%%%%%%:+$) l
      = forall arg. KindOf (Apply (:<<<%%%%%%%%%%:+$) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$) arg) =>
        (:<<<%%%%%%%%%%:+$###)
    type instance Apply (:<<<%%%%%%%%%%:+$) l = (:<<<%%%%%%%%%%:+$$) l
    type family (:<<<%%%%%%%%%%:+) x (a :: Nat) (a :: Nat) :: Nat where
      (:<<<%%%%%%%%%%:+) x Zero m = m
      (:<<<%%%%%%%%%%:+) x (Succ n) m = Apply SuccSym0 (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) n) x)
    type Let0123456789ZSym1 t = Let0123456789Z t
    instance SuppressUnusedWarnings Let0123456789ZSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
    data Let0123456789ZSym0 l
      = forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
        Let0123456789ZSym0KindInference
    type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
    type (:<<<%%%%%%%%%%:+$$$$) t (t :: Nat) (t :: Nat) =
        (:<<<%%%%%%%%%%:+) t t t
    instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$$###) GHC.Tuple.())
    data (:<<<%%%%%%%%%%:+$$$) l (l :: Nat) (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$$) l l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$$) l l arg) =>
        (:<<<%%%%%%%%%%:+$$$###)
    type instance Apply ((:<<<%%%%%%%%%%:+$$$) l l) l = (:<<<%%%%%%%%%%:+$$$$) l l l
    instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$###) GHC.Tuple.())
    data (:<<<%%%%%%%%%%:+$$) l (l :: TyFun Nat (TyFun Nat Nat -> *))
      = forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$) l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$) l arg) =>
        (:<<<%%%%%%%%%%:+$$###)
    type instance Apply ((:<<<%%%%%%%%%%:+$$) l) l = (:<<<%%%%%%%%%%:+$$$) l l
    instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$###) GHC.Tuple.())
    data (:<<<%%%%%%%%%%:+$) l
      = forall arg. KindOf (Apply (:<<<%%%%%%%%%%:+$) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$) arg) =>
        (:<<<%%%%%%%%%%:+$###)
    type instance Apply (:<<<%%%%%%%%%%:+$) l = (:<<<%%%%%%%%%%:+$$) l
    type Let0123456789Z x = (x :: Nat)
    type family (:<<<%%%%%%%%%%:+) x (a :: Nat) (a :: Nat) :: Nat where
      (:<<<%%%%%%%%%%:+) x Zero m = m
      (:<<<%%%%%%%%%%:+) x (Succ n) m = Apply SuccSym0 (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) n) m)
    type (:<<<%%%%%%%%%%:+$$$$) t (t :: Nat) (t :: Nat) =
        (:<<<%%%%%%%%%%:+) t t t
    instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$$###) GHC.Tuple.())
    data (:<<<%%%%%%%%%%:+$$$) l (l :: Nat) (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$$) l l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$$) l l arg) =>
        (:<<<%%%%%%%%%%:+$$$###)
    type instance Apply ((:<<<%%%%%%%%%%:+$$$) l l) l = (:<<<%%%%%%%%%%:+$$$$) l l l
    instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$###) GHC.Tuple.())
    data (:<<<%%%%%%%%%%:+$$) l (l :: TyFun Nat (TyFun Nat Nat -> *))
      = forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$) l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$) l arg) =>
        (:<<<%%%%%%%%%%:+$$###)
    type instance Apply ((:<<<%%%%%%%%%%:+$$) l) l = (:<<<%%%%%%%%%%:+$$$) l l
    instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$###) GHC.Tuple.())
    data (:<<<%%%%%%%%%%:+$) l
      = forall arg. KindOf (Apply (:<<<%%%%%%%%%%:+$) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$) arg) =>
        (:<<<%%%%%%%%%%:+$###)
    type instance Apply (:<<<%%%%%%%%%%:+$) l = (:<<<%%%%%%%%%%:+$$) l
    type family (:<<<%%%%%%%%%%:+) x (a :: Nat) (a :: Nat) :: Nat where
      (:<<<%%%%%%%%%%:+) x Zero m = m
      (:<<<%%%%%%%%%%:+) x (Succ n) m = Apply SuccSym0 (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) n) m)
    type family Lambda_0123456789 x a_0123456789 t where
      Lambda_0123456789 x a_0123456789 x = x
    type Lambda_0123456789Sym3 t t t = Lambda_0123456789 t t t
    instance SuppressUnusedWarnings Lambda_0123456789Sym2 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym2KindInference GHC.Tuple.())
    data Lambda_0123456789Sym2 l l l
      = forall arg. KindOf (Apply (Lambda_0123456789Sym2 l l) arg) ~ KindOf (Lambda_0123456789Sym3 l l arg) =>
        Lambda_0123456789Sym2KindInference
    type instance Apply (Lambda_0123456789Sym2 l l) l = Lambda_0123456789Sym3 l l l
    instance SuppressUnusedWarnings Lambda_0123456789Sym1 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.())
    data Lambda_0123456789Sym1 l l
      = forall arg. KindOf (Apply (Lambda_0123456789Sym1 l) arg) ~ KindOf (Lambda_0123456789Sym2 l arg) =>
        Lambda_0123456789Sym1KindInference
    type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l
    instance SuppressUnusedWarnings Lambda_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.())
    data Lambda_0123456789Sym0 l
      = forall arg. KindOf (Apply Lambda_0123456789Sym0 arg) ~ KindOf (Lambda_0123456789Sym1 arg) =>
        Lambda_0123456789Sym0KindInference
    type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l
    type Let0123456789ZSym2 t (t :: Nat) = Let0123456789Z t t
    instance SuppressUnusedWarnings Let0123456789ZSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789ZSym1KindInference GHC.Tuple.())
    data Let0123456789ZSym1 l (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply (Let0123456789ZSym1 l) arg) ~ KindOf (Let0123456789ZSym2 l arg) =>
        Let0123456789ZSym1KindInference
    type instance Apply (Let0123456789ZSym1 l) l = Let0123456789ZSym2 l l
    instance SuppressUnusedWarnings Let0123456789ZSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
    data Let0123456789ZSym0 l
      = forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
        Let0123456789ZSym0KindInference
    type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
    type family Let0123456789Z x (a :: Nat) :: Nat where
      Let0123456789Z x a_0123456789 = Apply (Apply (Apply Lambda_0123456789Sym0 x) a_0123456789) a_0123456789
    type family Lambda_0123456789 x t where
      Lambda_0123456789 x x = x
    type Lambda_0123456789Sym2 t t = Lambda_0123456789 t t
    instance SuppressUnusedWarnings Lambda_0123456789Sym1 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.())
    data Lambda_0123456789Sym1 l l
      = forall arg. KindOf (Apply (Lambda_0123456789Sym1 l) arg) ~ KindOf (Lambda_0123456789Sym2 l arg) =>
        Lambda_0123456789Sym1KindInference
    type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l
    instance SuppressUnusedWarnings Lambda_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd
            (GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.())
    data Lambda_0123456789Sym0 l
      = forall arg. KindOf (Apply Lambda_0123456789Sym0 arg) ~ KindOf (Lambda_0123456789Sym1 arg) =>
        Lambda_0123456789Sym0KindInference
    type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l
    type Let0123456789ZSym1 t = Let0123456789Z t
    instance SuppressUnusedWarnings Let0123456789ZSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
    data Let0123456789ZSym0 l
      = forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
        Let0123456789ZSym0KindInference
    type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
    type Let0123456789Z x =
        (Apply (Apply Lambda_0123456789Sym0 x) ZeroSym0 :: Nat)
    type Let0123456789XSym1 t = Let0123456789X t
    instance SuppressUnusedWarnings Let0123456789XSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789XSym0KindInference GHC.Tuple.())
    data Let0123456789XSym0 l
      = forall arg. KindOf (Apply Let0123456789XSym0 arg) ~ KindOf (Let0123456789XSym1 arg) =>
        Let0123456789XSym0KindInference
    type instance Apply Let0123456789XSym0 l = Let0123456789XSym1 l
    type Let0123456789X x = (ZeroSym0 :: Nat)
    type Let0123456789FSym2 t (t :: Nat) = Let0123456789F t t
    instance SuppressUnusedWarnings Let0123456789FSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789FSym1KindInference GHC.Tuple.())
    data Let0123456789FSym1 l (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply (Let0123456789FSym1 l) arg) ~ KindOf (Let0123456789FSym2 l arg) =>
        Let0123456789FSym1KindInference
    type instance Apply (Let0123456789FSym1 l) l = Let0123456789FSym2 l l
    instance SuppressUnusedWarnings Let0123456789FSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789FSym0KindInference GHC.Tuple.())
    data Let0123456789FSym0 l
      = forall arg. KindOf (Apply Let0123456789FSym0 arg) ~ KindOf (Let0123456789FSym1 arg) =>
        Let0123456789FSym0KindInference
    type instance Apply Let0123456789FSym0 l = Let0123456789FSym1 l
    type family Let0123456789F x (a :: Nat) :: Nat where
      Let0123456789F x y = Apply SuccSym0 y
    type Let0123456789ZSym1 t = Let0123456789Z t
    instance SuppressUnusedWarnings Let0123456789ZSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
    data Let0123456789ZSym0 l
      = forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
        Let0123456789ZSym0KindInference
    type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
    type Let0123456789Z x = (Apply (Let0123456789FSym1 x) x :: Nat)
    type Let0123456789ZSym2 t t = Let0123456789Z t t
    instance SuppressUnusedWarnings Let0123456789ZSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789ZSym1KindInference GHC.Tuple.())
    data Let0123456789ZSym1 l l
      = forall arg. KindOf (Apply (Let0123456789ZSym1 l) arg) ~ KindOf (Let0123456789ZSym2 l arg) =>
        Let0123456789ZSym1KindInference
    type instance Apply (Let0123456789ZSym1 l) l = Let0123456789ZSym2 l l
    instance SuppressUnusedWarnings Let0123456789ZSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
    data Let0123456789ZSym0 l
      = forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
        Let0123456789ZSym0KindInference
    type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
    type Let0123456789Z x y = (Apply SuccSym0 y :: Nat)
    type Let0123456789FSym2 t (t :: Nat) = Let0123456789F t t
    instance SuppressUnusedWarnings Let0123456789FSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789FSym1KindInference GHC.Tuple.())
    data Let0123456789FSym1 l (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply (Let0123456789FSym1 l) arg) ~ KindOf (Let0123456789FSym2 l arg) =>
        Let0123456789FSym1KindInference
    type instance Apply (Let0123456789FSym1 l) l = Let0123456789FSym2 l l
    instance SuppressUnusedWarnings Let0123456789FSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789FSym0KindInference GHC.Tuple.())
    data Let0123456789FSym0 l
      = forall arg. KindOf (Apply Let0123456789FSym0 arg) ~ KindOf (Let0123456789FSym1 arg) =>
        Let0123456789FSym0KindInference
    type instance Apply Let0123456789FSym0 l = Let0123456789FSym1 l
    type family Let0123456789F x (a :: Nat) :: Nat where
      Let0123456789F x y = Apply SuccSym0 (Let0123456789ZSym2 x y)
    type Let0123456789FSym2 t (t :: Nat) = Let0123456789F t t
    instance SuppressUnusedWarnings Let0123456789FSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789FSym1KindInference GHC.Tuple.())
    data Let0123456789FSym1 l (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply (Let0123456789FSym1 l) arg) ~ KindOf (Let0123456789FSym2 l arg) =>
        Let0123456789FSym1KindInference
    type instance Apply (Let0123456789FSym1 l) l = Let0123456789FSym2 l l
    instance SuppressUnusedWarnings Let0123456789FSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789FSym0KindInference GHC.Tuple.())
    data Let0123456789FSym0 l
      = forall arg. KindOf (Apply Let0123456789FSym0 arg) ~ KindOf (Let0123456789FSym1 arg) =>
        Let0123456789FSym0KindInference
    type instance Apply Let0123456789FSym0 l = Let0123456789FSym1 l
    type family Let0123456789F x (a :: Nat) :: Nat where
      Let0123456789F x y = Apply SuccSym0 y
    type Let0123456789YSym1 t = Let0123456789Y t
    instance SuppressUnusedWarnings Let0123456789YSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789YSym0KindInference GHC.Tuple.())
    data Let0123456789YSym0 l
      = forall arg. KindOf (Apply Let0123456789YSym0 arg) ~ KindOf (Let0123456789YSym1 arg) =>
        Let0123456789YSym0KindInference
    type instance Apply Let0123456789YSym0 l = Let0123456789YSym1 l
    type Let0123456789Y x = (Apply SuccSym0 x :: Nat)
    type Let0123456789YSym0 = Let0123456789Y
    type Let0123456789ZSym0 = Let0123456789Z
    type Let0123456789Y = Apply SuccSym0 ZeroSym0
    type Let0123456789Z = Apply SuccSym0 Let0123456789YSym0
    type Let0123456789YSym1 t = Let0123456789Y t
    instance SuppressUnusedWarnings Let0123456789YSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Let0123456789YSym0KindInference GHC.Tuple.())
    data Let0123456789YSym0 l
      = forall arg. KindOf (Apply Let0123456789YSym0 arg) ~ KindOf (Let0123456789YSym1 arg) =>
        Let0123456789YSym0KindInference
    type instance Apply Let0123456789YSym0 l = Let0123456789YSym1 l
    type Let0123456789Y x = (Apply SuccSym0 ZeroSym0 :: Nat)
    type Foo14Sym1 (t :: Nat) = Foo14 t
    instance SuppressUnusedWarnings Foo14Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo14Sym0KindInference GHC.Tuple.())
    data Foo14Sym0 (l :: TyFun Nat (Nat, Nat))
      = forall arg. KindOf (Apply Foo14Sym0 arg) ~ KindOf (Foo14Sym1 arg) =>
        Foo14Sym0KindInference
    type instance Apply Foo14Sym0 l = Foo14Sym1 l
    type Foo13_Sym1 (t :: a) = Foo13_ t
    instance SuppressUnusedWarnings Foo13_Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo13_Sym0KindInference GHC.Tuple.())
    data Foo13_Sym0 (l :: TyFun a a)
      = forall arg. KindOf (Apply Foo13_Sym0 arg) ~ KindOf (Foo13_Sym1 arg) =>
        Foo13_Sym0KindInference
    type instance Apply Foo13_Sym0 l = Foo13_Sym1 l
    type Foo13Sym1 (t :: a) = Foo13 t
    instance SuppressUnusedWarnings Foo13Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo13Sym0KindInference GHC.Tuple.())
    data Foo13Sym0 (l :: TyFun a a)
      = forall arg. KindOf (Apply Foo13Sym0 arg) ~ KindOf (Foo13Sym1 arg) =>
        Foo13Sym0KindInference
    type instance Apply Foo13Sym0 l = Foo13Sym1 l
    type Foo12Sym1 (t :: Nat) = Foo12 t
    instance SuppressUnusedWarnings Foo12Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo12Sym0KindInference GHC.Tuple.())
    data Foo12Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo12Sym0 arg) ~ KindOf (Foo12Sym1 arg) =>
        Foo12Sym0KindInference
    type instance Apply Foo12Sym0 l = Foo12Sym1 l
    type Foo11Sym1 (t :: Nat) = Foo11 t
    instance SuppressUnusedWarnings Foo11Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo11Sym0KindInference GHC.Tuple.())
    data Foo11Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo11Sym0 arg) ~ KindOf (Foo11Sym1 arg) =>
        Foo11Sym0KindInference
    type instance Apply Foo11Sym0 l = Foo11Sym1 l
    type Foo10Sym1 (t :: Nat) = Foo10 t
    instance SuppressUnusedWarnings Foo10Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo10Sym0KindInference GHC.Tuple.())
    data Foo10Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo10Sym0 arg) ~ KindOf (Foo10Sym1 arg) =>
        Foo10Sym0KindInference
    type instance Apply Foo10Sym0 l = Foo10Sym1 l
    type Foo9Sym1 (t :: Nat) = Foo9 t
    instance SuppressUnusedWarnings Foo9Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo9Sym0KindInference GHC.Tuple.())
    data Foo9Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo9Sym0 arg) ~ KindOf (Foo9Sym1 arg) =>
        Foo9Sym0KindInference
    type instance Apply Foo9Sym0 l = Foo9Sym1 l
    type Foo8Sym1 (t :: Nat) = Foo8 t
    instance SuppressUnusedWarnings Foo8Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo8Sym0KindInference GHC.Tuple.())
    data Foo8Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo8Sym0 arg) ~ KindOf (Foo8Sym1 arg) =>
        Foo8Sym0KindInference
    type instance Apply Foo8Sym0 l = Foo8Sym1 l
    type Foo7Sym1 (t :: Nat) = Foo7 t
    instance SuppressUnusedWarnings Foo7Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo7Sym0KindInference GHC.Tuple.())
    data Foo7Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo7Sym0 arg) ~ KindOf (Foo7Sym1 arg) =>
        Foo7Sym0KindInference
    type instance Apply Foo7Sym0 l = Foo7Sym1 l
    type Foo6Sym1 (t :: Nat) = Foo6 t
    instance SuppressUnusedWarnings Foo6Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo6Sym0KindInference GHC.Tuple.())
    data Foo6Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo6Sym0 arg) ~ KindOf (Foo6Sym1 arg) =>
        Foo6Sym0KindInference
    type instance Apply Foo6Sym0 l = Foo6Sym1 l
    type Foo5Sym1 (t :: Nat) = Foo5 t
    instance SuppressUnusedWarnings Foo5Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo5Sym0KindInference GHC.Tuple.())
    data Foo5Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo5Sym0 arg) ~ KindOf (Foo5Sym1 arg) =>
        Foo5Sym0KindInference
    type instance Apply Foo5Sym0 l = Foo5Sym1 l
    type Foo4Sym1 (t :: Nat) = Foo4 t
    instance SuppressUnusedWarnings Foo4Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo4Sym0KindInference GHC.Tuple.())
    data Foo4Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo4Sym0 arg) ~ KindOf (Foo4Sym1 arg) =>
        Foo4Sym0KindInference
    type instance Apply Foo4Sym0 l = Foo4Sym1 l
    type Foo3Sym1 (t :: Nat) = Foo3 t
    instance SuppressUnusedWarnings Foo3Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo3Sym0KindInference GHC.Tuple.())
    data Foo3Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo3Sym0 arg) ~ KindOf (Foo3Sym1 arg) =>
        Foo3Sym0KindInference
    type instance Apply Foo3Sym0 l = Foo3Sym1 l
    type Foo2Sym0 = Foo2
    type Foo1Sym1 (t :: Nat) = Foo1 t
    instance SuppressUnusedWarnings Foo1Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Foo1Sym0KindInference GHC.Tuple.())
    data Foo1Sym0 (l :: TyFun Nat Nat)
      = forall arg. KindOf (Apply Foo1Sym0 arg) ~ KindOf (Foo1Sym1 arg) =>
        Foo1Sym0KindInference
    type instance Apply Foo1Sym0 l = Foo1Sym1 l
    type family Foo14 (a :: Nat) :: (Nat, Nat) where
      Foo14 x = Apply (Apply Tuple2Sym0 (Let0123456789ZSym1 x)) (Let0123456789YSym1 x)
    type family Foo13_ (a :: a) :: a where
      Foo13_ y = y
    type family Foo13 (a :: a) :: a where
      Foo13 x = Apply Foo13_Sym0 (Let0123456789BarSym1 x)
    type family Foo12 (a :: Nat) :: Nat where
      Foo12 x = Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) x) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))
    type family Foo11 (a :: Nat) :: Nat where
      Foo11 x = Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) (Apply SuccSym0 ZeroSym0)) (Let0123456789ZSym1 x)
    type family Foo10 (a :: Nat) :: Nat where
      Foo10 x = Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) (Apply SuccSym0 ZeroSym0)) x
    type family Foo9 (a :: Nat) :: Nat where
      Foo9 x = Apply (Let0123456789ZSym1 x) x
    type family Foo8 (a :: Nat) :: Nat where
      Foo8 x = Let0123456789ZSym1 x
    type family Foo7 (a :: Nat) :: Nat where
      Foo7 x = Let0123456789XSym1 x
    type family Foo6 (a :: Nat) :: Nat where
      Foo6 x = Let0123456789ZSym1 x
    type family Foo5 (a :: Nat) :: Nat where
      Foo5 x = Apply (Let0123456789FSym1 x) x
    type family Foo4 (a :: Nat) :: Nat where
      Foo4 x = Apply (Let0123456789FSym1 x) x
    type family Foo3 (a :: Nat) :: Nat where
      Foo3 x = Let0123456789YSym1 x
    type Foo2 = (Let0123456789ZSym0 :: Nat)
    type family Foo1 (a :: Nat) :: Nat where
      Foo1 x = Let0123456789YSym1 x
    sFoo14 :: forall (t :: Nat). Sing t -> Sing (Apply Foo14Sym0 t)
    sFoo13_ :: forall (t :: a). Sing t -> Sing (Apply Foo13_Sym0 t)
    sFoo13 :: forall (t :: a). Sing t -> Sing (Apply Foo13Sym0 t)
    sFoo12 :: forall (t :: Nat). Sing t -> Sing (Apply Foo12Sym0 t)
    sFoo11 :: forall (t :: Nat). Sing t -> Sing (Apply Foo11Sym0 t)
    sFoo10 :: forall (t :: Nat). Sing t -> Sing (Apply Foo10Sym0 t)
    sFoo9 :: forall (t :: Nat). Sing t -> Sing (Apply Foo9Sym0 t)
    sFoo8 :: forall (t :: Nat). Sing t -> Sing (Apply Foo8Sym0 t)
    sFoo7 :: forall (t :: Nat). Sing t -> Sing (Apply Foo7Sym0 t)
    sFoo6 :: forall (t :: Nat). Sing t -> Sing (Apply Foo6Sym0 t)
    sFoo5 :: forall (t :: Nat). Sing t -> Sing (Apply Foo5Sym0 t)
    sFoo4 :: forall (t :: Nat). Sing t -> Sing (Apply Foo4Sym0 t)
    sFoo3 :: forall (t :: Nat). Sing t -> Sing (Apply Foo3Sym0 t)
    sFoo2 :: Sing Foo2Sym0
    sFoo1 :: forall (t :: Nat). Sing t -> Sing (Apply Foo1Sym0 t)
    sFoo14 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo14Sym0 x)
          lambda x
            = let
                sY :: Sing (Let0123456789YSym1 x)
                sZ :: Sing (Let0123456789ZSym1 x)
                sX_0123456789 :: Sing (Let0123456789X_0123456789Sym1 x)
                sY
                  = case sX_0123456789 of {
                      STuple2 sY_0123456789 _
                        -> let
                             lambda ::
                               forall y_0123456789 wild.
                               Sing y_0123456789
                               -> Sing (Case_0123456789 x (Apply (Apply Tuple2Sym0 y_0123456789) wild))
                             lambda y_0123456789 = y_0123456789
                           in lambda sY_0123456789 }
                sZ
                  = case sX_0123456789 of {
                      STuple2 _ sY_0123456789
                        -> let
                             lambda ::
                               forall y_0123456789 wild.
                               Sing y_0123456789
                               -> Sing (Case_0123456789 x (Apply (Apply Tuple2Sym0 wild) y_0123456789))
                             lambda y_0123456789 = y_0123456789
                           in lambda sY_0123456789 }
                sX_0123456789
                  = applySing
                      (applySing
                         (singFun2 (Proxy :: Proxy Tuple2Sym0) STuple2)
                         (applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) x))
                      x
              in
                applySing
                  (applySing (singFun2 (Proxy :: Proxy Tuple2Sym0) STuple2) sZ) sY
        in lambda sX
    sFoo13_ sY
      = let
          lambda :: forall y. t ~ y => Sing y -> Sing (Apply Foo13_Sym0 y)
          lambda y = y
        in lambda sY
    sFoo13 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo13Sym0 x)
          lambda x
            = let
                sBar :: Sing (Let0123456789BarSym1 x)
                sBar = x
              in applySing (singFun1 (Proxy :: Proxy Foo13_Sym0) sFoo13_) sBar
        in lambda sX
    sFoo12 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo12Sym0 x)
          lambda x
            = let
                (%:+) ::
                  forall t t.
                  Sing t
                  -> Sing t -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t)
                (%:+) SZero sM
                  = let
                      lambda ::
                        forall m. (t ~ ZeroSym0, t ~ m) =>
                        Sing m -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) ZeroSym0) m)
                      lambda m = m
                    in lambda sM
                (%:+) (SSucc sN) sM
                  = let
                      lambda ::
                        forall n m. (t ~ Apply SuccSym0 n, t ~ m) =>
                        Sing n
                        -> Sing m
                           -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) (Apply SuccSym0 n)) m)
                      lambda n m
                        = applySing
                            (singFun1 (Proxy :: Proxy SuccSym0) SSucc)
                            (applySing
                               (applySing
                                  (singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+)) n)
                               x)
                    in lambda sN sM
              in
                applySing
                  (applySing
                     (singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+)) x)
                  (applySing
                     (singFun1 (Proxy :: Proxy SuccSym0) SSucc)
                     (applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero))
        in lambda sX
    sFoo11 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo11Sym0 x)
          lambda x
            = let
                sZ :: Sing (Let0123456789ZSym1 x)
                (%:+) ::
                  forall t t.
                  Sing t
                  -> Sing t -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t)
                sZ = x
                (%:+) SZero sM
                  = let
                      lambda ::
                        forall m. (t ~ ZeroSym0, t ~ m) =>
                        Sing m -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) ZeroSym0) m)
                      lambda m = m
                    in lambda sM
                (%:+) (SSucc sN) sM
                  = let
                      lambda ::
                        forall n m. (t ~ Apply SuccSym0 n, t ~ m) =>
                        Sing n
                        -> Sing m
                           -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) (Apply SuccSym0 n)) m)
                      lambda n m
                        = applySing
                            (singFun1 (Proxy :: Proxy SuccSym0) SSucc)
                            (applySing
                               (applySing
                                  (singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+)) n)
                               m)
                    in lambda sN sM
              in
                applySing
                  (applySing
                     (singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+))
                     (applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero))
                  sZ
        in lambda sX
    sFoo10 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo10Sym0 x)
          lambda x
            = let
                (%:+) ::
                  forall t t.
                  Sing t
                  -> Sing t -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t)
                (%:+) SZero sM
                  = let
                      lambda ::
                        forall m. (t ~ ZeroSym0, t ~ m) =>
                        Sing m -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) ZeroSym0) m)
                      lambda m = m
                    in lambda sM
                (%:+) (SSucc sN) sM
                  = let
                      lambda ::
                        forall n m. (t ~ Apply SuccSym0 n, t ~ m) =>
                        Sing n
                        -> Sing m
                           -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) (Apply SuccSym0 n)) m)
                      lambda n m
                        = applySing
                            (singFun1 (Proxy :: Proxy SuccSym0) SSucc)
                            (applySing
                               (applySing
                                  (singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+)) n)
                               m)
                    in lambda sN sM
              in
                applySing
                  (applySing
                     (singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+))
                     (applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero))
                  x
        in lambda sX
    sFoo9 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo9Sym0 x)
          lambda x
            = let
                sZ :: forall t. Sing t -> Sing (Apply (Let0123456789ZSym1 x) t)
                sZ sA_0123456789
                  = let
                      lambda ::
                        forall a_0123456789. t ~ a_0123456789 =>
                        Sing a_0123456789
                        -> Sing (Apply (Let0123456789ZSym1 x) a_0123456789)
                      lambda a_0123456789
                        = applySing
                            (singFun1
                               (Proxy ::
                                  Proxy (Apply (Apply Lambda_0123456789Sym0 x) a_0123456789))
                               (\ sX
                                  -> let
                                       lambda ::
                                         forall x.
                                         Sing x
                                         -> Sing (Apply (Apply (Apply Lambda_0123456789Sym0 x) a_0123456789) x)
                                       lambda x = x
                                     in lambda sX))
                            a_0123456789
                    in lambda sA_0123456789
              in
                applySing (singFun1 (Proxy :: Proxy (Let0123456789ZSym1 x)) sZ) x
        in lambda sX
    sFoo8 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo8Sym0 x)
          lambda x
            = let
                sZ :: Sing (Let0123456789ZSym1 x)
                sZ
                  = applySing
                      (singFun1
                         (Proxy :: Proxy (Apply Lambda_0123456789Sym0 x))
                         (\ sX
                            -> let
                                 lambda ::
                                   forall x.
                                   Sing x -> Sing (Apply (Apply Lambda_0123456789Sym0 x) x)
                                 lambda x = x
                               in lambda sX))
                      SZero
              in sZ
        in lambda sX
    sFoo7 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo7Sym0 x)
          lambda x
            = let
                sX :: Sing (Let0123456789XSym1 x)
                sX = SZero
              in sX
        in lambda sX
    sFoo6 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo6Sym0 x)
          lambda x
            = let
                sF :: forall t. Sing t -> Sing (Apply (Let0123456789FSym1 x) t)
                sF sY
                  = let
                      lambda ::
                        forall y. t ~ y => Sing y -> Sing (Apply (Let0123456789FSym1 x) y)
                      lambda y = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) y
                    in lambda sY in
              let
                sZ :: Sing (Let0123456789ZSym1 x)
                sZ
                  = applySing (singFun1 (Proxy :: Proxy (Let0123456789FSym1 x)) sF) x
              in sZ
        in lambda sX
    sFoo5 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo5Sym0 x)
          lambda x
            = let
                sF :: forall t. Sing t -> Sing (Apply (Let0123456789FSym1 x) t)
                sF sY
                  = let
                      lambda ::
                        forall y. t ~ y => Sing y -> Sing (Apply (Let0123456789FSym1 x) y)
                      lambda y
                        = let
                            sZ :: Sing (Let0123456789ZSym2 x y)
                            sZ = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) y
                          in applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) sZ
                    in lambda sY
              in
                applySing (singFun1 (Proxy :: Proxy (Let0123456789FSym1 x)) sF) x
        in lambda sX
    sFoo4 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo4Sym0 x)
          lambda x
            = let
                sF :: forall t. Sing t -> Sing (Apply (Let0123456789FSym1 x) t)
                sF sY
                  = let
                      lambda ::
                        forall y. t ~ y => Sing y -> Sing (Apply (Let0123456789FSym1 x) y)
                      lambda y = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) y
                    in lambda sY
              in
                applySing (singFun1 (Proxy :: Proxy (Let0123456789FSym1 x)) sF) x
        in lambda sX
    sFoo3 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo3Sym0 x)
          lambda x
            = let
                sY :: Sing (Let0123456789YSym1 x)
                sY = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) x
              in sY
        in lambda sX
    sFoo2
      = let
          sY :: Sing Let0123456789YSym0
          sZ :: Sing Let0123456789ZSym0
          sY = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero
          sZ = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) sY
        in sZ
    sFoo1 sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply Foo1Sym0 x)
          lambda x
            = let
                sY :: Sing (Let0123456789YSym1 x)
                sY = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero
              in sY
        in lambda sX