GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| data Nat
            = Zero | Succ Nat
            deriving (Eq, Ord) |]
  ======>
    data Nat
      = Zero | Succ Nat
      deriving (Eq, Ord)
    type ZeroSym0 = Zero
    type SuccSym1 (t0123456789876543210 :: Nat) =
        Succ t0123456789876543210
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings = snd (((,) SuccSym0KindInference) ())
    data SuccSym0 :: (~>) Nat Nat
      where
        SuccSym0KindInference :: forall t0123456789876543210
                                        arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
                                 SuccSym0 t0123456789876543210
    type instance Apply SuccSym0 t0123456789876543210 = Succ t0123456789876543210
    type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
      Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
      Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[])
      Compare_0123456789876543210 Zero (Succ _) = LTSym0
      Compare_0123456789876543210 (Succ _) Zero = GTSym0
    type Compare_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
        Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd (((,) Compare_0123456789876543210Sym1KindInference) ())
    data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Nat) :: (~>) Nat Ordering
      where
        Compare_0123456789876543210Sym1KindInference :: forall a0123456789876543210
                                                               a0123456789876543210
                                                               arg. SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                        Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd (((,) Compare_0123456789876543210Sym0KindInference) ())
    data Compare_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Ordering)
      where
        Compare_0123456789876543210Sym0KindInference :: forall a0123456789876543210
                                                               arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
                                                        Compare_0123456789876543210Sym0 a0123456789876543210
    type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210
    instance POrd Nat where
      type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
    type family Equals_0123456789876543210 (a :: Nat) (b :: Nat) :: Bool where
      Equals_0123456789876543210 Zero Zero = TrueSym0
      Equals_0123456789876543210 (Succ a) (Succ b) = (==) a b
      Equals_0123456789876543210 (_ :: Nat) (_ :: Nat) = FalseSym0
    instance PEq Nat where
      type (==) a b = Equals_0123456789876543210 a b
    data instance Sing :: Nat -> Type
      where
        SZero :: Sing Zero
        SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> Sing (Succ n)
    type SNat = (Sing :: Nat -> Type)
    instance SingKind Nat where
      type Demote Nat = Nat
      fromSing SZero = Zero
      fromSing (SSucc b) = Succ (fromSing b)
      toSing Zero = SomeSing SZero
      toSing (Succ (b :: Demote Nat))
        = case toSing b :: SomeSing Nat of {
            SomeSing c -> SomeSing (SSucc c) }
    instance SOrd Nat => SOrd Nat where
      sCompare ::
        forall (t1 :: Nat) (t2 :: Nat).
        Sing t1
        -> Sing t2
           -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering)
                                                 -> Type) t1) t2)
      sCompare SZero SZero
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            SNil
      sCompare
        (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            ((applySing
                ((applySing ((singFun2 @(:@#@$)) SCons))
                   ((applySing
                       ((applySing ((singFun2 @CompareSym0) sCompare))
                          sA_0123456789876543210))
                      sB_0123456789876543210)))
               SNil)
      sCompare SZero (SSucc _) = SLT
      sCompare (SSucc _) SZero = SGT
    instance SEq Nat => SEq Nat where
      (%==) SZero SZero = STrue
      (%==) SZero (SSucc _) = SFalse
      (%==) (SSucc _) SZero = SFalse
      (%==) (SSucc a) (SSucc b) = ((%==) a) b
    instance SDecide Nat => SDecide Nat where
      (%~) SZero SZero = Proved Refl
      (%~) SZero (SSucc _) = Disproved (\ x -> case x of)
      (%~) (SSucc _) SZero = Disproved (\ x -> case x of)
      (%~) (SSucc a) (SSucc b)
        = case ((%~) a) b of
            Proved Refl -> Proved Refl
            Disproved contra
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
    instance SingI Zero where
      sing = SZero
    instance SingI n => SingI (Succ (n :: Nat)) where
      sing = SSucc sing
    instance SingI (SuccSym0 :: (~>) Nat Nat) where
      sing = (singFun1 @SuccSym0) SSucc
    instance SingI (TyCon1 Succ :: (~>) Nat Nat) where
      sing = (singFun1 @(TyCon1 Succ)) SSucc
GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| append :: Schema -> Schema -> Schema
          append (Sch s1) (Sch s2) = Sch (s1 ++ s2)
          attrNotIn :: Attribute -> Schema -> Bool
          attrNotIn _ (Sch []) = True
          attrNotIn (Attr name u) (Sch ((Attr name' _) : t))
            = (name /= name') && (attrNotIn (Attr name u) (Sch t))
          disjoint :: Schema -> Schema -> Bool
          disjoint (Sch []) _ = True
          disjoint (Sch (h : t)) s = (attrNotIn h s) && (disjoint (Sch t) s)
          occurs :: [AChar] -> Schema -> Bool
          occurs _ (Sch []) = False
          occurs name (Sch ((Attr name' _) : attrs))
            = name == name' || occurs name (Sch attrs)
          lookup :: [AChar] -> Schema -> U
          lookup _ (Sch []) = undefined
          lookup name (Sch ((Attr name' u) : attrs))
            = if name == name' then u else lookup name (Sch attrs)
          
          data U
            = BOOL | STRING | NAT | VEC U Nat
            deriving (Read, Eq, Show)
          data AChar
            = CA |
              CB |
              CC |
              CD |
              CE |
              CF |
              CG |
              CH |
              CI |
              CJ |
              CK |
              CL |
              CM |
              CN |
              CO |
              CP |
              CQ |
              CR |
              CS |
              CT |
              CU |
              CV |
              CW |
              CX |
              CY |
              CZ
            deriving (Read, Show, Eq)
          data Attribute = Attr [AChar] U
          data Schema = Sch [Attribute] |]
  ======>
    data U
      = BOOL | STRING | NAT | VEC U Nat
      deriving (Read, Eq, Show)
    data AChar
      = CA |
        CB |
        CC |
        CD |
        CE |
        CF |
        CG |
        CH |
        CI |
        CJ |
        CK |
        CL |
        CM |
        CN |
        CO |
        CP |
        CQ |
        CR |
        CS |
        CT |
        CU |
        CV |
        CW |
        CX |
        CY |
        CZ
      deriving (Read, Show, Eq)
    data Attribute = Attr [AChar] U
    data Schema = Sch [Attribute]
    append :: Schema -> Schema -> Schema
    append (Sch s1) (Sch s2) = Sch (s1 ++ s2)
    attrNotIn :: Attribute -> Schema -> Bool
    attrNotIn _ (Sch []) = True
    attrNotIn (Attr name u) (Sch (Attr name' _ : t))
      = ((name /= name') && (attrNotIn ((Attr name) u)) (Sch t))
    disjoint :: Schema -> Schema -> Bool
    disjoint (Sch []) _ = True
    disjoint (Sch (h : t)) s
      = ((attrNotIn h) s && (disjoint (Sch t)) s)
    occurs :: [AChar] -> Schema -> Bool
    occurs _ (Sch []) = False
    occurs name (Sch (Attr name' _ : attrs))
      = ((name == name') || (occurs name) (Sch attrs))
    lookup :: [AChar] -> Schema -> U
    lookup _ (Sch []) = undefined
    lookup name (Sch (Attr name' u : attrs))
      = if (name == name') then u else (lookup name) (Sch attrs)
    type BOOLSym0 = BOOL
    type STRINGSym0 = STRING
    type NATSym0 = NAT
    type VECSym2 (t0123456789876543210 :: U) (t0123456789876543210 :: Nat) =
        VEC t0123456789876543210 t0123456789876543210
    instance SuppressUnusedWarnings (VECSym1 t0123456789876543210) where
      suppressUnusedWarnings = snd (((,) VECSym1KindInference) ())
    data VECSym1 (t0123456789876543210 :: U) :: (~>) Nat U
      where
        VECSym1KindInference :: forall t0123456789876543210
                                       t0123456789876543210
                                       arg. SameKind (Apply (VECSym1 t0123456789876543210) arg) (VECSym2 t0123456789876543210 arg) =>
                                VECSym1 t0123456789876543210 t0123456789876543210
    type instance Apply (VECSym1 t0123456789876543210) t0123456789876543210 = VEC t0123456789876543210 t0123456789876543210
    instance SuppressUnusedWarnings VECSym0 where
      suppressUnusedWarnings = snd (((,) VECSym0KindInference) ())
    data VECSym0 :: (~>) U ((~>) Nat U)
      where
        VECSym0KindInference :: forall t0123456789876543210
                                       arg. SameKind (Apply VECSym0 arg) (VECSym1 arg) =>
                                VECSym0 t0123456789876543210
    type instance Apply VECSym0 t0123456789876543210 = VECSym1 t0123456789876543210
    type CASym0 = CA
    type CBSym0 = CB
    type CCSym0 = CC
    type CDSym0 = CD
    type CESym0 = CE
    type CFSym0 = CF
    type CGSym0 = CG
    type CHSym0 = CH
    type CISym0 = CI
    type CJSym0 = CJ
    type CKSym0 = CK
    type CLSym0 = CL
    type CMSym0 = CM
    type CNSym0 = CN
    type COSym0 = CO
    type CPSym0 = CP
    type CQSym0 = CQ
    type CRSym0 = CR
    type CSSym0 = CS
    type CTSym0 = CT
    type CUSym0 = CU
    type CVSym0 = CV
    type CWSym0 = CW
    type CXSym0 = CX
    type CYSym0 = CY
    type CZSym0 = CZ
    type AttrSym2 (t0123456789876543210 :: [AChar]) (t0123456789876543210 :: U) =
        Attr t0123456789876543210 t0123456789876543210
    instance SuppressUnusedWarnings (AttrSym1 t0123456789876543210) where
      suppressUnusedWarnings = snd (((,) AttrSym1KindInference) ())
    data AttrSym1 (t0123456789876543210 :: [AChar]) :: (~>) U Attribute
      where
        AttrSym1KindInference :: forall t0123456789876543210
                                        t0123456789876543210
                                        arg. SameKind (Apply (AttrSym1 t0123456789876543210) arg) (AttrSym2 t0123456789876543210 arg) =>
                                 AttrSym1 t0123456789876543210 t0123456789876543210
    type instance Apply (AttrSym1 t0123456789876543210) t0123456789876543210 = Attr t0123456789876543210 t0123456789876543210
    instance SuppressUnusedWarnings AttrSym0 where
      suppressUnusedWarnings = snd (((,) AttrSym0KindInference) ())
    data AttrSym0 :: (~>) [AChar] ((~>) U Attribute)
      where
        AttrSym0KindInference :: forall t0123456789876543210
                                        arg. SameKind (Apply AttrSym0 arg) (AttrSym1 arg) =>
                                 AttrSym0 t0123456789876543210
    type instance Apply AttrSym0 t0123456789876543210 = AttrSym1 t0123456789876543210
    type SchSym1 (t0123456789876543210 :: [Attribute]) =
        Sch t0123456789876543210
    instance SuppressUnusedWarnings SchSym0 where
      suppressUnusedWarnings = snd (((,) SchSym0KindInference) ())
    data SchSym0 :: (~>) [Attribute] Schema
      where
        SchSym0KindInference :: forall t0123456789876543210
                                       arg. SameKind (Apply SchSym0 arg) (SchSym1 arg) =>
                                SchSym0 t0123456789876543210
    type instance Apply SchSym0 t0123456789876543210 = Sch t0123456789876543210
    type Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 =
        Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym3 u0123456789876543210 name'0123456789876543210 name0123456789876543210) where
      suppressUnusedWarnings
        = snd
            (((,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym3KindInference)
               ())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym3KindInference :: forall name0123456789876543210
                                                                                       name'0123456789876543210
                                                                                       u0123456789876543210
                                                                                       attrs0123456789876543210
                                                                                       arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym3 u0123456789876543210 name'0123456789876543210 name0123456789876543210) attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 u0123456789876543210 name'0123456789876543210 name0123456789876543210 attrs0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name'0123456789876543210 name0123456789876543210) where
      suppressUnusedWarnings
        = snd
            (((,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference)
               ())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210 u0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference :: forall name0123456789876543210
                                                                                       name'0123456789876543210
                                                                                       u0123456789876543210
                                                                                       arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 name0123456789876543210 name'0123456789876543210 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210 u0123456789876543210
    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name'0123456789876543210 name0123456789876543210) u0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym3 name'0123456789876543210 name0123456789876543210 u0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) where
      suppressUnusedWarnings
        = snd
            (((,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference)
               ())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference :: forall name0123456789876543210
                                                                                       name'0123456789876543210
                                                                                       arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210
    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210) name'0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym2 name0123456789876543210 name'0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            (((,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
               ())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: forall name0123456789876543210
                                                                                       arg. SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210
    type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 name0123456789876543210
    type family Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs where
      Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs = Apply (Apply (==@#@$) name) name'
    type family Case_0123456789876543210 name name' u attrs t where
      Case_0123456789876543210 name name' u attrs  'True = u
      Case_0123456789876543210 name name' u attrs  'False = Apply (Apply LookupSym0 name) (Apply SchSym0 attrs)
    type LookupSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: Schema) =
        Lookup a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (LookupSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) LookupSym1KindInference) ())
    data LookupSym1 (a0123456789876543210 :: [AChar]) :: (~>) Schema U
      where
        LookupSym1KindInference :: forall a0123456789876543210
                                          a0123456789876543210
                                          arg. SameKind (Apply (LookupSym1 a0123456789876543210) arg) (LookupSym2 a0123456789876543210 arg) =>
                                   LookupSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (LookupSym1 a0123456789876543210) a0123456789876543210 = Lookup a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings LookupSym0 where
      suppressUnusedWarnings = snd (((,) LookupSym0KindInference) ())
    data LookupSym0 :: (~>) [AChar] ((~>) Schema U)
      where
        LookupSym0KindInference :: forall a0123456789876543210
                                          arg. SameKind (Apply LookupSym0 arg) (LookupSym1 arg) =>
                                   LookupSym0 a0123456789876543210
    type instance Apply LookupSym0 a0123456789876543210 = LookupSym1 a0123456789876543210
    type OccursSym2 (a0123456789876543210 :: [AChar]) (a0123456789876543210 :: Schema) =
        Occurs a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (OccursSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) OccursSym1KindInference) ())
    data OccursSym1 (a0123456789876543210 :: [AChar]) :: (~>) Schema Bool
      where
        OccursSym1KindInference :: forall a0123456789876543210
                                          a0123456789876543210
                                          arg. SameKind (Apply (OccursSym1 a0123456789876543210) arg) (OccursSym2 a0123456789876543210 arg) =>
                                   OccursSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (OccursSym1 a0123456789876543210) a0123456789876543210 = Occurs a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings OccursSym0 where
      suppressUnusedWarnings = snd (((,) OccursSym0KindInference) ())
    data OccursSym0 :: (~>) [AChar] ((~>) Schema Bool)
      where
        OccursSym0KindInference :: forall a0123456789876543210
                                          arg. SameKind (Apply OccursSym0 arg) (OccursSym1 arg) =>
                                   OccursSym0 a0123456789876543210
    type instance Apply OccursSym0 a0123456789876543210 = OccursSym1 a0123456789876543210
    type AttrNotInSym2 (a0123456789876543210 :: Attribute) (a0123456789876543210 :: Schema) =
        AttrNotIn a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (AttrNotInSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) AttrNotInSym1KindInference) ())
    data AttrNotInSym1 (a0123456789876543210 :: Attribute) :: (~>) Schema Bool
      where
        AttrNotInSym1KindInference :: forall a0123456789876543210
                                             a0123456789876543210
                                             arg. SameKind (Apply (AttrNotInSym1 a0123456789876543210) arg) (AttrNotInSym2 a0123456789876543210 arg) =>
                                      AttrNotInSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (AttrNotInSym1 a0123456789876543210) a0123456789876543210 = AttrNotIn a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings AttrNotInSym0 where
      suppressUnusedWarnings = snd (((,) AttrNotInSym0KindInference) ())
    data AttrNotInSym0 :: (~>) Attribute ((~>) Schema Bool)
      where
        AttrNotInSym0KindInference :: forall a0123456789876543210
                                             arg. SameKind (Apply AttrNotInSym0 arg) (AttrNotInSym1 arg) =>
                                      AttrNotInSym0 a0123456789876543210
    type instance Apply AttrNotInSym0 a0123456789876543210 = AttrNotInSym1 a0123456789876543210
    type DisjointSym2 (a0123456789876543210 :: Schema) (a0123456789876543210 :: Schema) =
        Disjoint a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (DisjointSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) DisjointSym1KindInference) ())
    data DisjointSym1 (a0123456789876543210 :: Schema) :: (~>) Schema Bool
      where
        DisjointSym1KindInference :: forall a0123456789876543210
                                            a0123456789876543210
                                            arg. SameKind (Apply (DisjointSym1 a0123456789876543210) arg) (DisjointSym2 a0123456789876543210 arg) =>
                                     DisjointSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (DisjointSym1 a0123456789876543210) a0123456789876543210 = Disjoint a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings DisjointSym0 where
      suppressUnusedWarnings = snd (((,) DisjointSym0KindInference) ())
    data DisjointSym0 :: (~>) Schema ((~>) Schema Bool)
      where
        DisjointSym0KindInference :: forall a0123456789876543210
                                            arg. SameKind (Apply DisjointSym0 arg) (DisjointSym1 arg) =>
                                     DisjointSym0 a0123456789876543210
    type instance Apply DisjointSym0 a0123456789876543210 = DisjointSym1 a0123456789876543210
    type AppendSym2 (a0123456789876543210 :: Schema) (a0123456789876543210 :: Schema) =
        Append a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (AppendSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) AppendSym1KindInference) ())
    data AppendSym1 (a0123456789876543210 :: Schema) :: (~>) Schema Schema
      where
        AppendSym1KindInference :: forall a0123456789876543210
                                          a0123456789876543210
                                          arg. SameKind (Apply (AppendSym1 a0123456789876543210) arg) (AppendSym2 a0123456789876543210 arg) =>
                                   AppendSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (AppendSym1 a0123456789876543210) a0123456789876543210 = Append a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings AppendSym0 where
      suppressUnusedWarnings = snd (((,) AppendSym0KindInference) ())
    data AppendSym0 :: (~>) Schema ((~>) Schema Schema)
      where
        AppendSym0KindInference :: forall a0123456789876543210
                                          arg. SameKind (Apply AppendSym0 arg) (AppendSym1 arg) =>
                                   AppendSym0 a0123456789876543210
    type instance Apply AppendSym0 a0123456789876543210 = AppendSym1 a0123456789876543210
    type family Lookup (a :: [AChar]) (a :: Schema) :: U where
      Lookup _ (Sch '[]) = UndefinedSym0
      Lookup name (Sch ( '(:) (Attr name' u) attrs)) = Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs)
    type family Occurs (a :: [AChar]) (a :: Schema) :: Bool where
      Occurs _ (Sch '[]) = FalseSym0
      Occurs name (Sch ( '(:) (Attr name' _) attrs)) = Apply (Apply (||@#@$) (Apply (Apply (==@#@$) name) name')) (Apply (Apply OccursSym0 name) (Apply SchSym0 attrs))
    type family AttrNotIn (a :: Attribute) (a :: Schema) :: Bool where
      AttrNotIn _ (Sch '[]) = TrueSym0
      AttrNotIn (Attr name u) (Sch ( '(:) (Attr name' _) t)) = Apply (Apply (&&@#@$) (Apply (Apply (/=@#@$) name) name')) (Apply (Apply AttrNotInSym0 (Apply (Apply AttrSym0 name) u)) (Apply SchSym0 t))
    type family Disjoint (a :: Schema) (a :: Schema) :: Bool where
      Disjoint (Sch '[]) _ = TrueSym0
      Disjoint (Sch ( '(:) h t)) s = Apply (Apply (&&@#@$) (Apply (Apply AttrNotInSym0 h) s)) (Apply (Apply DisjointSym0 (Apply SchSym0 t)) s)
    type family Append (a :: Schema) (a :: Schema) :: Schema where
      Append (Sch s1) (Sch s2) = Apply SchSym0 (Apply (Apply (++@#@$) s1) s2)
    type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: U) (a :: Symbol) :: Symbol where
      ShowsPrec_0123456789876543210 _ BOOL a_0123456789876543210 = Apply (Apply ShowStringSym0 "BOOL") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ STRING a_0123456789876543210 = Apply (Apply ShowStringSym0 "STRING") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ NAT a_0123456789876543210 = Apply (Apply ShowStringSym0 "NAT") a_0123456789876543210
      ShowsPrec_0123456789876543210 p_0123456789876543210 (VEC arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "VEC ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
    type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: U) (a0123456789876543210 :: Symbol) =
        ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings
        = snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
    data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: U) :: (~>) Symbol Symbol
      where
        ShowsPrec_0123456789876543210Sym2KindInference :: forall a0123456789876543210
                                                                 a0123456789876543210
                                                                 a0123456789876543210
                                                                 arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
                                                          ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
    type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())
    data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: (~>) U ((~>) Symbol Symbol)
      where
        ShowsPrec_0123456789876543210Sym1KindInference :: forall a0123456789876543210
                                                                 a0123456789876543210
                                                                 arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                          ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ())
    data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Types.Nat ((~>) U ((~>) Symbol Symbol))
      where
        ShowsPrec_0123456789876543210Sym0KindInference :: forall a0123456789876543210
                                                                 arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
                                                          ShowsPrec_0123456789876543210Sym0 a0123456789876543210
    type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
    instance PShow U where
      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
    type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: AChar) (a :: Symbol) :: Symbol where
      ShowsPrec_0123456789876543210 _ CA a_0123456789876543210 = Apply (Apply ShowStringSym0 "CA") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CB a_0123456789876543210 = Apply (Apply ShowStringSym0 "CB") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CC a_0123456789876543210 = Apply (Apply ShowStringSym0 "CC") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CD a_0123456789876543210 = Apply (Apply ShowStringSym0 "CD") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CE a_0123456789876543210 = Apply (Apply ShowStringSym0 "CE") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CF a_0123456789876543210 = Apply (Apply ShowStringSym0 "CF") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CG a_0123456789876543210 = Apply (Apply ShowStringSym0 "CG") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CH a_0123456789876543210 = Apply (Apply ShowStringSym0 "CH") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CI a_0123456789876543210 = Apply (Apply ShowStringSym0 "CI") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CJ a_0123456789876543210 = Apply (Apply ShowStringSym0 "CJ") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CK a_0123456789876543210 = Apply (Apply ShowStringSym0 "CK") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CL a_0123456789876543210 = Apply (Apply ShowStringSym0 "CL") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CM a_0123456789876543210 = Apply (Apply ShowStringSym0 "CM") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CN a_0123456789876543210 = Apply (Apply ShowStringSym0 "CN") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CO a_0123456789876543210 = Apply (Apply ShowStringSym0 "CO") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CP a_0123456789876543210 = Apply (Apply ShowStringSym0 "CP") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CQ a_0123456789876543210 = Apply (Apply ShowStringSym0 "CQ") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CR a_0123456789876543210 = Apply (Apply ShowStringSym0 "CR") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CS a_0123456789876543210 = Apply (Apply ShowStringSym0 "CS") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CT a_0123456789876543210 = Apply (Apply ShowStringSym0 "CT") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CU a_0123456789876543210 = Apply (Apply ShowStringSym0 "CU") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CV a_0123456789876543210 = Apply (Apply ShowStringSym0 "CV") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CW a_0123456789876543210 = Apply (Apply ShowStringSym0 "CW") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CX a_0123456789876543210 = Apply (Apply ShowStringSym0 "CX") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CY a_0123456789876543210 = Apply (Apply ShowStringSym0 "CY") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ CZ a_0123456789876543210 = Apply (Apply ShowStringSym0 "CZ") a_0123456789876543210
    type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: AChar) (a0123456789876543210 :: Symbol) =
        ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings
        = snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
    data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: AChar) :: (~>) Symbol Symbol
      where
        ShowsPrec_0123456789876543210Sym2KindInference :: forall a0123456789876543210
                                                                 a0123456789876543210
                                                                 a0123456789876543210
                                                                 arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
                                                          ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
    type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())
    data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: (~>) AChar ((~>) Symbol Symbol)
      where
        ShowsPrec_0123456789876543210Sym1KindInference :: forall a0123456789876543210
                                                                 a0123456789876543210
                                                                 arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                          ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ())
    data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Types.Nat ((~>) AChar ((~>) Symbol Symbol))
      where
        ShowsPrec_0123456789876543210Sym0KindInference :: forall a0123456789876543210
                                                                 arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
                                                          ShowsPrec_0123456789876543210Sym0 a0123456789876543210
    type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
    instance PShow AChar where
      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
    type family Equals_0123456789876543210 (a :: U) (b :: U) :: Bool where
      Equals_0123456789876543210 BOOL BOOL = TrueSym0
      Equals_0123456789876543210 STRING STRING = TrueSym0
      Equals_0123456789876543210 NAT NAT = TrueSym0
      Equals_0123456789876543210 (VEC a a) (VEC b b) = (&&) ((==) a b) ((==) a b)
      Equals_0123456789876543210 (_ :: U) (_ :: U) = FalseSym0
    instance PEq U where
      type (==) a b = Equals_0123456789876543210 a b
    type family Equals_0123456789876543210 (a :: AChar) (b :: AChar) :: Bool where
      Equals_0123456789876543210 CA CA = TrueSym0
      Equals_0123456789876543210 CB CB = TrueSym0
      Equals_0123456789876543210 CC CC = TrueSym0
      Equals_0123456789876543210 CD CD = TrueSym0
      Equals_0123456789876543210 CE CE = TrueSym0
      Equals_0123456789876543210 CF CF = TrueSym0
      Equals_0123456789876543210 CG CG = TrueSym0
      Equals_0123456789876543210 CH CH = TrueSym0
      Equals_0123456789876543210 CI CI = TrueSym0
      Equals_0123456789876543210 CJ CJ = TrueSym0
      Equals_0123456789876543210 CK CK = TrueSym0
      Equals_0123456789876543210 CL CL = TrueSym0
      Equals_0123456789876543210 CM CM = TrueSym0
      Equals_0123456789876543210 CN CN = TrueSym0
      Equals_0123456789876543210 CO CO = TrueSym0
      Equals_0123456789876543210 CP CP = TrueSym0
      Equals_0123456789876543210 CQ CQ = TrueSym0
      Equals_0123456789876543210 CR CR = TrueSym0
      Equals_0123456789876543210 CS CS = TrueSym0
      Equals_0123456789876543210 CT CT = TrueSym0
      Equals_0123456789876543210 CU CU = TrueSym0
      Equals_0123456789876543210 CV CV = TrueSym0
      Equals_0123456789876543210 CW CW = TrueSym0
      Equals_0123456789876543210 CX CX = TrueSym0
      Equals_0123456789876543210 CY CY = TrueSym0
      Equals_0123456789876543210 CZ CZ = TrueSym0
      Equals_0123456789876543210 (_ :: AChar) (_ :: AChar) = FalseSym0
    instance PEq AChar where
      type (==) a b = Equals_0123456789876543210 a b
    sLookup ::
      forall (t :: [AChar]) (t :: Schema).
      Sing t -> Sing t -> Sing (Apply (Apply LookupSym0 t) t :: U)
    sOccurs ::
      forall (t :: [AChar]) (t :: Schema).
      Sing t -> Sing t -> Sing (Apply (Apply OccursSym0 t) t :: Bool)
    sAttrNotIn ::
      forall (t :: Attribute) (t :: Schema).
      Sing t -> Sing t -> Sing (Apply (Apply AttrNotInSym0 t) t :: Bool)
    sDisjoint ::
      forall (t :: Schema) (t :: Schema).
      Sing t -> Sing t -> Sing (Apply (Apply DisjointSym0 t) t :: Bool)
    sAppend ::
      forall (t :: Schema) (t :: Schema).
      Sing t -> Sing t -> Sing (Apply (Apply AppendSym0 t) t :: Schema)
    sLookup _ (SSch SNil) = sUndefined
    sLookup
      (sName :: Sing name)
      (SSch (SCons (SAttr (sName' :: Sing name') (sU :: Sing u))
                   (sAttrs :: Sing attrs)))
      = let
          sScrutinee_0123456789876543210 ::
            Sing (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs)
          sScrutinee_0123456789876543210
            = (applySing ((applySing ((singFun2 @(==@#@$)) (%==))) sName))
                sName'
        in  (case sScrutinee_0123456789876543210 of
               STrue -> sU
               SFalse
                 -> (applySing ((applySing ((singFun2 @LookupSym0) sLookup)) sName))
                      ((applySing ((singFun1 @SchSym0) SSch)) sAttrs)) ::
              Sing (Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs) :: U)
    sOccurs _ (SSch SNil) = SFalse
    sOccurs
      (sName :: Sing name)
      (SSch (SCons (SAttr (sName' :: Sing name') _)
                   (sAttrs :: Sing attrs)))
      = (applySing
           ((applySing ((singFun2 @(||@#@$)) (%||)))
              ((applySing ((applySing ((singFun2 @(==@#@$)) (%==))) sName))
                 sName')))
          ((applySing ((applySing ((singFun2 @OccursSym0) sOccurs)) sName))
             ((applySing ((singFun1 @SchSym0) SSch)) sAttrs))
    sAttrNotIn _ (SSch SNil) = STrue
    sAttrNotIn
      (SAttr (sName :: Sing name) (sU :: Sing u))
      (SSch (SCons (SAttr (sName' :: Sing name') _) (sT :: Sing t)))
      = (applySing
           ((applySing ((singFun2 @(&&@#@$)) (%&&)))
              ((applySing ((applySing ((singFun2 @(/=@#@$)) (%/=))) sName))
                 sName')))
          ((applySing
              ((applySing ((singFun2 @AttrNotInSym0) sAttrNotIn))
                 ((applySing ((applySing ((singFun2 @AttrSym0) SAttr)) sName)) sU)))
             ((applySing ((singFun1 @SchSym0) SSch)) sT))
    sDisjoint (SSch SNil) _ = STrue
    sDisjoint
      (SSch (SCons (sH :: Sing h) (sT :: Sing t)))
      (sS :: Sing s)
      = (applySing
           ((applySing ((singFun2 @(&&@#@$)) (%&&)))
              ((applySing
                  ((applySing ((singFun2 @AttrNotInSym0) sAttrNotIn)) sH))
                 sS)))
          ((applySing
              ((applySing ((singFun2 @DisjointSym0) sDisjoint))
                 ((applySing ((singFun1 @SchSym0) SSch)) sT)))
             sS)
    sAppend (SSch (sS1 :: Sing s1)) (SSch (sS2 :: Sing s2))
      = (applySing ((singFun1 @SchSym0) SSch))
          ((applySing ((applySing ((singFun2 @(++@#@$)) (%++))) sS1)) sS2)
    instance SingI (LookupSym0 :: (~>) [AChar] ((~>) Schema U)) where
      sing = (singFun2 @LookupSym0) sLookup
    instance SingI d =>
             SingI (LookupSym1 (d :: [AChar]) :: (~>) Schema U) where
      sing = (singFun1 @(LookupSym1 (d :: [AChar]))) (sLookup (sing @d))
    instance SingI (OccursSym0 :: (~>) [AChar] ((~>) Schema Bool)) where
      sing = (singFun2 @OccursSym0) sOccurs
    instance SingI d =>
             SingI (OccursSym1 (d :: [AChar]) :: (~>) Schema Bool) where
      sing = (singFun1 @(OccursSym1 (d :: [AChar]))) (sOccurs (sing @d))
    instance SingI (AttrNotInSym0 :: (~>) Attribute ((~>) Schema Bool)) where
      sing = (singFun2 @AttrNotInSym0) sAttrNotIn
    instance SingI d =>
             SingI (AttrNotInSym1 (d :: Attribute) :: (~>) Schema Bool) where
      sing
        = (singFun1 @(AttrNotInSym1 (d :: Attribute)))
            (sAttrNotIn (sing @d))
    instance SingI (DisjointSym0 :: (~>) Schema ((~>) Schema Bool)) where
      sing = (singFun2 @DisjointSym0) sDisjoint
    instance SingI d =>
             SingI (DisjointSym1 (d :: Schema) :: (~>) Schema Bool) where
      sing
        = (singFun1 @(DisjointSym1 (d :: Schema))) (sDisjoint (sing @d))
    instance SingI (AppendSym0 :: (~>) Schema ((~>) Schema Schema)) where
      sing = (singFun2 @AppendSym0) sAppend
    instance SingI d =>
             SingI (AppendSym1 (d :: Schema) :: (~>) Schema Schema) where
      sing = (singFun1 @(AppendSym1 (d :: Schema))) (sAppend (sing @d))
    data instance Sing :: U -> Type
      where
        SBOOL :: Sing BOOL
        SSTRING :: Sing STRING
        SNAT :: Sing NAT
        SVEC :: forall (n :: U) (n :: Nat).
                (Sing (n :: U)) -> (Sing (n :: Nat)) -> Sing (VEC n n)
    type SU = (Sing :: U -> Type)
    instance SingKind U where
      type Demote U = U
      fromSing SBOOL = BOOL
      fromSing SSTRING = STRING
      fromSing SNAT = NAT
      fromSing (SVEC b b) = (VEC (fromSing b)) (fromSing b)
      toSing BOOL = SomeSing SBOOL
      toSing STRING = SomeSing SSTRING
      toSing NAT = SomeSing SNAT
      toSing (VEC (b :: Demote U) (b :: Demote Nat))
        = case
              ((,) (toSing b :: SomeSing U)) (toSing b :: SomeSing Nat)
          of {
            (,) (SomeSing c) (SomeSing c) -> SomeSing ((SVEC c) c) }
    data instance Sing :: AChar -> Type
      where
        SCA :: Sing CA
        SCB :: Sing CB
        SCC :: Sing CC
        SCD :: Sing CD
        SCE :: Sing CE
        SCF :: Sing CF
        SCG :: Sing CG
        SCH :: Sing CH
        SCI :: Sing CI
        SCJ :: Sing CJ
        SCK :: Sing CK
        SCL :: Sing CL
        SCM :: Sing CM
        SCN :: Sing CN
        SCO :: Sing CO
        SCP :: Sing CP
        SCQ :: Sing CQ
        SCR :: Sing CR
        SCS :: Sing CS
        SCT :: Sing CT
        SCU :: Sing CU
        SCV :: Sing CV
        SCW :: Sing CW
        SCX :: Sing CX
        SCY :: Sing CY
        SCZ :: Sing CZ
    type SAChar = (Sing :: AChar -> Type)
    instance SingKind AChar where
      type Demote AChar = AChar
      fromSing SCA = CA
      fromSing SCB = CB
      fromSing SCC = CC
      fromSing SCD = CD
      fromSing SCE = CE
      fromSing SCF = CF
      fromSing SCG = CG
      fromSing SCH = CH
      fromSing SCI = CI
      fromSing SCJ = CJ
      fromSing SCK = CK
      fromSing SCL = CL
      fromSing SCM = CM
      fromSing SCN = CN
      fromSing SCO = CO
      fromSing SCP = CP
      fromSing SCQ = CQ
      fromSing SCR = CR
      fromSing SCS = CS
      fromSing SCT = CT
      fromSing SCU = CU
      fromSing SCV = CV
      fromSing SCW = CW
      fromSing SCX = CX
      fromSing SCY = CY
      fromSing SCZ = CZ
      toSing CA = SomeSing SCA
      toSing CB = SomeSing SCB
      toSing CC = SomeSing SCC
      toSing CD = SomeSing SCD
      toSing CE = SomeSing SCE
      toSing CF = SomeSing SCF
      toSing CG = SomeSing SCG
      toSing CH = SomeSing SCH
      toSing CI = SomeSing SCI
      toSing CJ = SomeSing SCJ
      toSing CK = SomeSing SCK
      toSing CL = SomeSing SCL
      toSing CM = SomeSing SCM
      toSing CN = SomeSing SCN
      toSing CO = SomeSing SCO
      toSing CP = SomeSing SCP
      toSing CQ = SomeSing SCQ
      toSing CR = SomeSing SCR
      toSing CS = SomeSing SCS
      toSing CT = SomeSing SCT
      toSing CU = SomeSing SCU
      toSing CV = SomeSing SCV
      toSing CW = SomeSing SCW
      toSing CX = SomeSing SCX
      toSing CY = SomeSing SCY
      toSing CZ = SomeSing SCZ
    data instance Sing :: Attribute -> Type
      where
        SAttr :: forall (n :: [AChar]) (n :: U).
                 (Sing (n :: [AChar])) -> (Sing (n :: U)) -> Sing (Attr n n)
    type SAttribute = (Sing :: Attribute -> Type)
    instance SingKind Attribute where
      type Demote Attribute = Attribute
      fromSing (SAttr b b) = (Attr (fromSing b)) (fromSing b)
      toSing (Attr (b :: Demote [AChar]) (b :: Demote U))
        = case
              ((,) (toSing b :: SomeSing [AChar])) (toSing b :: SomeSing U)
          of {
            (,) (SomeSing c) (SomeSing c) -> SomeSing ((SAttr c) c) }
    data instance Sing :: Schema -> Type
      where
        SSch :: forall (n :: [Attribute]).
                (Sing (n :: [Attribute])) -> Sing (Sch n)
    type SSchema = (Sing :: Schema -> Type)
    instance SingKind Schema where
      type Demote Schema = Schema
      fromSing (SSch b) = Sch (fromSing b)
      toSing (Sch (b :: Demote [Attribute]))
        = case toSing b :: SomeSing [Attribute] of {
            SomeSing c -> SomeSing (SSch c) }
    instance (SShow U, SShow Nat) => SShow U where
      sShowsPrec ::
        forall (t1 :: GHC.Types.Nat) (t2 :: U) (t3 :: Symbol).
        Sing t1
        -> Sing t2
           -> Sing t3
              -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) U ((~>) Symbol Symbol))
                                                             -> Type) t1) t2) t3)
      sShowsPrec
        _
        SBOOL
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "BOOL")))
            sA_0123456789876543210
      sShowsPrec
        _
        SSTRING
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "STRING")))
            sA_0123456789876543210
      sShowsPrec
        _
        SNAT
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "NAT")))
            sA_0123456789876543210
      sShowsPrec
        (sP_0123456789876543210 :: Sing p_0123456789876543210)
        (SVEC (sArg_0123456789876543210 :: Sing arg_0123456789876543210)
              (sArg_0123456789876543210 :: Sing arg_0123456789876543210))
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @ShowParenSym0) sShowParen))
                    ((applySing
                        ((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210))
                       (sFromInteger (sing :: Sing 10)))))
                ((applySing
                    ((applySing ((singFun3 @(.@#@$)) (%.)))
                       ((applySing ((singFun2 @ShowStringSym0) sShowString))
                          (sing :: Sing "VEC "))))
                   ((applySing
                       ((applySing ((singFun3 @(.@#@$)) (%.)))
                          ((applySing
                              ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))
                                 (sFromInteger (sing :: Sing 11))))
                             sArg_0123456789876543210)))
                      ((applySing
                          ((applySing ((singFun3 @(.@#@$)) (%.)))
                             ((singFun1 @ShowSpaceSym0) sShowSpace)))
                         ((applySing
                             ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))
                                (sFromInteger (sing :: Sing 11))))
                            sArg_0123456789876543210))))))
            sA_0123456789876543210
    instance SShow AChar where
      sShowsPrec ::
        forall (t1 :: GHC.Types.Nat) (t2 :: AChar) (t3 :: Symbol).
        Sing t1
        -> Sing t2
           -> Sing t3
              -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) AChar ((~>) Symbol Symbol))
                                                             -> Type) t1) t2) t3)
      sShowsPrec
        _
        SCA
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CA")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCB
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CB")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCC
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CC")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCD
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CD")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCE
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CE")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCF
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CF")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCG
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CG")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCH
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CH")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCI
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CI")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCJ
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CJ")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCK
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CK")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCL
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CL")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCM
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CM")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCN
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CN")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCO
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CO")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCP
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CP")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCQ
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CQ")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCR
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CR")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCS
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CS")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCT
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CT")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCU
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CU")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCV
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CV")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCW
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CW")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCX
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CX")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCY
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CY")))
            sA_0123456789876543210
      sShowsPrec
        _
        SCZ
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "CZ")))
            sA_0123456789876543210
    instance (SEq U, SEq Nat) => SEq U where
      (%==) SBOOL SBOOL = STrue
      (%==) SBOOL SSTRING = SFalse
      (%==) SBOOL SNAT = SFalse
      (%==) SBOOL (SVEC _ _) = SFalse
      (%==) SSTRING SBOOL = SFalse
      (%==) SSTRING SSTRING = STrue
      (%==) SSTRING SNAT = SFalse
      (%==) SSTRING (SVEC _ _) = SFalse
      (%==) SNAT SBOOL = SFalse
      (%==) SNAT SSTRING = SFalse
      (%==) SNAT SNAT = STrue
      (%==) SNAT (SVEC _ _) = SFalse
      (%==) (SVEC _ _) SBOOL = SFalse
      (%==) (SVEC _ _) SSTRING = SFalse
      (%==) (SVEC _ _) SNAT = SFalse
      (%==) (SVEC a a) (SVEC b b) = ((%&&) (((%==) a) b)) (((%==) a) b)
    instance (SDecide U, SDecide Nat) => SDecide U where
      (%~) SBOOL SBOOL = Proved Refl
      (%~) SBOOL SSTRING = Disproved (\ x -> case x of)
      (%~) SBOOL SNAT = Disproved (\ x -> case x of)
      (%~) SBOOL (SVEC _ _) = Disproved (\ x -> case x of)
      (%~) SSTRING SBOOL = Disproved (\ x -> case x of)
      (%~) SSTRING SSTRING = Proved Refl
      (%~) SSTRING SNAT = Disproved (\ x -> case x of)
      (%~) SSTRING (SVEC _ _) = Disproved (\ x -> case x of)
      (%~) SNAT SBOOL = Disproved (\ x -> case x of)
      (%~) SNAT SSTRING = Disproved (\ x -> case x of)
      (%~) SNAT SNAT = Proved Refl
      (%~) SNAT (SVEC _ _) = Disproved (\ x -> case x of)
      (%~) (SVEC _ _) SBOOL = Disproved (\ x -> case x of)
      (%~) (SVEC _ _) SSTRING = Disproved (\ x -> case x of)
      (%~) (SVEC _ _) SNAT = Disproved (\ x -> case x of)
      (%~) (SVEC a a) (SVEC b b)
        = case ((,) (((%~) a) b)) (((%~) a) b) of
            (,) (Proved Refl) (Proved Refl) -> Proved Refl
            (,) (Disproved contra) _
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
            (,) _ (Disproved contra)
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
    instance SEq AChar where
      (%==) SCA SCA = STrue
      (%==) SCA SCB = SFalse
      (%==) SCA SCC = SFalse
      (%==) SCA SCD = SFalse
      (%==) SCA SCE = SFalse
      (%==) SCA SCF = SFalse
      (%==) SCA SCG = SFalse
      (%==) SCA SCH = SFalse
      (%==) SCA SCI = SFalse
      (%==) SCA SCJ = SFalse
      (%==) SCA SCK = SFalse
      (%==) SCA SCL = SFalse
      (%==) SCA SCM = SFalse
      (%==) SCA SCN = SFalse
      (%==) SCA SCO = SFalse
      (%==) SCA SCP = SFalse
      (%==) SCA SCQ = SFalse
      (%==) SCA SCR = SFalse
      (%==) SCA SCS = SFalse
      (%==) SCA SCT = SFalse
      (%==) SCA SCU = SFalse
      (%==) SCA SCV = SFalse
      (%==) SCA SCW = SFalse
      (%==) SCA SCX = SFalse
      (%==) SCA SCY = SFalse
      (%==) SCA SCZ = SFalse
      (%==) SCB SCA = SFalse
      (%==) SCB SCB = STrue
      (%==) SCB SCC = SFalse
      (%==) SCB SCD = SFalse
      (%==) SCB SCE = SFalse
      (%==) SCB SCF = SFalse
      (%==) SCB SCG = SFalse
      (%==) SCB SCH = SFalse
      (%==) SCB SCI = SFalse
      (%==) SCB SCJ = SFalse
      (%==) SCB SCK = SFalse
      (%==) SCB SCL = SFalse
      (%==) SCB SCM = SFalse
      (%==) SCB SCN = SFalse
      (%==) SCB SCO = SFalse
      (%==) SCB SCP = SFalse
      (%==) SCB SCQ = SFalse
      (%==) SCB SCR = SFalse
      (%==) SCB SCS = SFalse
      (%==) SCB SCT = SFalse
      (%==) SCB SCU = SFalse
      (%==) SCB SCV = SFalse
      (%==) SCB SCW = SFalse
      (%==) SCB SCX = SFalse
      (%==) SCB SCY = SFalse
      (%==) SCB SCZ = SFalse
      (%==) SCC SCA = SFalse
      (%==) SCC SCB = SFalse
      (%==) SCC SCC = STrue
      (%==) SCC SCD = SFalse
      (%==) SCC SCE = SFalse
      (%==) SCC SCF = SFalse
      (%==) SCC SCG = SFalse
      (%==) SCC SCH = SFalse
      (%==) SCC SCI = SFalse
      (%==) SCC SCJ = SFalse
      (%==) SCC SCK = SFalse
      (%==) SCC SCL = SFalse
      (%==) SCC SCM = SFalse
      (%==) SCC SCN = SFalse
      (%==) SCC SCO = SFalse
      (%==) SCC SCP = SFalse
      (%==) SCC SCQ = SFalse
      (%==) SCC SCR = SFalse
      (%==) SCC SCS = SFalse
      (%==) SCC SCT = SFalse
      (%==) SCC SCU = SFalse
      (%==) SCC SCV = SFalse
      (%==) SCC SCW = SFalse
      (%==) SCC SCX = SFalse
      (%==) SCC SCY = SFalse
      (%==) SCC SCZ = SFalse
      (%==) SCD SCA = SFalse
      (%==) SCD SCB = SFalse
      (%==) SCD SCC = SFalse
      (%==) SCD SCD = STrue
      (%==) SCD SCE = SFalse
      (%==) SCD SCF = SFalse
      (%==) SCD SCG = SFalse
      (%==) SCD SCH = SFalse
      (%==) SCD SCI = SFalse
      (%==) SCD SCJ = SFalse
      (%==) SCD SCK = SFalse
      (%==) SCD SCL = SFalse
      (%==) SCD SCM = SFalse
      (%==) SCD SCN = SFalse
      (%==) SCD SCO = SFalse
      (%==) SCD SCP = SFalse
      (%==) SCD SCQ = SFalse
      (%==) SCD SCR = SFalse
      (%==) SCD SCS = SFalse
      (%==) SCD SCT = SFalse
      (%==) SCD SCU = SFalse
      (%==) SCD SCV = SFalse
      (%==) SCD SCW = SFalse
      (%==) SCD SCX = SFalse
      (%==) SCD SCY = SFalse
      (%==) SCD SCZ = SFalse
      (%==) SCE SCA = SFalse
      (%==) SCE SCB = SFalse
      (%==) SCE SCC = SFalse
      (%==) SCE SCD = SFalse
      (%==) SCE SCE = STrue
      (%==) SCE SCF = SFalse
      (%==) SCE SCG = SFalse
      (%==) SCE SCH = SFalse
      (%==) SCE SCI = SFalse
      (%==) SCE SCJ = SFalse
      (%==) SCE SCK = SFalse
      (%==) SCE SCL = SFalse
      (%==) SCE SCM = SFalse
      (%==) SCE SCN = SFalse
      (%==) SCE SCO = SFalse
      (%==) SCE SCP = SFalse
      (%==) SCE SCQ = SFalse
      (%==) SCE SCR = SFalse
      (%==) SCE SCS = SFalse
      (%==) SCE SCT = SFalse
      (%==) SCE SCU = SFalse
      (%==) SCE SCV = SFalse
      (%==) SCE SCW = SFalse
      (%==) SCE SCX = SFalse
      (%==) SCE SCY = SFalse
      (%==) SCE SCZ = SFalse
      (%==) SCF SCA = SFalse
      (%==) SCF SCB = SFalse
      (%==) SCF SCC = SFalse
      (%==) SCF SCD = SFalse
      (%==) SCF SCE = SFalse
      (%==) SCF SCF = STrue
      (%==) SCF SCG = SFalse
      (%==) SCF SCH = SFalse
      (%==) SCF SCI = SFalse
      (%==) SCF SCJ = SFalse
      (%==) SCF SCK = SFalse
      (%==) SCF SCL = SFalse
      (%==) SCF SCM = SFalse
      (%==) SCF SCN = SFalse
      (%==) SCF SCO = SFalse
      (%==) SCF SCP = SFalse
      (%==) SCF SCQ = SFalse
      (%==) SCF SCR = SFalse
      (%==) SCF SCS = SFalse
      (%==) SCF SCT = SFalse
      (%==) SCF SCU = SFalse
      (%==) SCF SCV = SFalse
      (%==) SCF SCW = SFalse
      (%==) SCF SCX = SFalse
      (%==) SCF SCY = SFalse
      (%==) SCF SCZ = SFalse
      (%==) SCG SCA = SFalse
      (%==) SCG SCB = SFalse
      (%==) SCG SCC = SFalse
      (%==) SCG SCD = SFalse
      (%==) SCG SCE = SFalse
      (%==) SCG SCF = SFalse
      (%==) SCG SCG = STrue
      (%==) SCG SCH = SFalse
      (%==) SCG SCI = SFalse
      (%==) SCG SCJ = SFalse
      (%==) SCG SCK = SFalse
      (%==) SCG SCL = SFalse
      (%==) SCG SCM = SFalse
      (%==) SCG SCN = SFalse
      (%==) SCG SCO = SFalse
      (%==) SCG SCP = SFalse
      (%==) SCG SCQ = SFalse
      (%==) SCG SCR = SFalse
      (%==) SCG SCS = SFalse
      (%==) SCG SCT = SFalse
      (%==) SCG SCU = SFalse
      (%==) SCG SCV = SFalse
      (%==) SCG SCW = SFalse
      (%==) SCG SCX = SFalse
      (%==) SCG SCY = SFalse
      (%==) SCG SCZ = SFalse
      (%==) SCH SCA = SFalse
      (%==) SCH SCB = SFalse
      (%==) SCH SCC = SFalse
      (%==) SCH SCD = SFalse
      (%==) SCH SCE = SFalse
      (%==) SCH SCF = SFalse
      (%==) SCH SCG = SFalse
      (%==) SCH SCH = STrue
      (%==) SCH SCI = SFalse
      (%==) SCH SCJ = SFalse
      (%==) SCH SCK = SFalse
      (%==) SCH SCL = SFalse
      (%==) SCH SCM = SFalse
      (%==) SCH SCN = SFalse
      (%==) SCH SCO = SFalse
      (%==) SCH SCP = SFalse
      (%==) SCH SCQ = SFalse
      (%==) SCH SCR = SFalse
      (%==) SCH SCS = SFalse
      (%==) SCH SCT = SFalse
      (%==) SCH SCU = SFalse
      (%==) SCH SCV = SFalse
      (%==) SCH SCW = SFalse
      (%==) SCH SCX = SFalse
      (%==) SCH SCY = SFalse
      (%==) SCH SCZ = SFalse
      (%==) SCI SCA = SFalse
      (%==) SCI SCB = SFalse
      (%==) SCI SCC = SFalse
      (%==) SCI SCD = SFalse
      (%==) SCI SCE = SFalse
      (%==) SCI SCF = SFalse
      (%==) SCI SCG = SFalse
      (%==) SCI SCH = SFalse
      (%==) SCI SCI = STrue
      (%==) SCI SCJ = SFalse
      (%==) SCI SCK = SFalse
      (%==) SCI SCL = SFalse
      (%==) SCI SCM = SFalse
      (%==) SCI SCN = SFalse
      (%==) SCI SCO = SFalse
      (%==) SCI SCP = SFalse
      (%==) SCI SCQ = SFalse
      (%==) SCI SCR = SFalse
      (%==) SCI SCS = SFalse
      (%==) SCI SCT = SFalse
      (%==) SCI SCU = SFalse
      (%==) SCI SCV = SFalse
      (%==) SCI SCW = SFalse
      (%==) SCI SCX = SFalse
      (%==) SCI SCY = SFalse
      (%==) SCI SCZ = SFalse
      (%==) SCJ SCA = SFalse
      (%==) SCJ SCB = SFalse
      (%==) SCJ SCC = SFalse
      (%==) SCJ SCD = SFalse
      (%==) SCJ SCE = SFalse
      (%==) SCJ SCF = SFalse
      (%==) SCJ SCG = SFalse
      (%==) SCJ SCH = SFalse
      (%==) SCJ SCI = SFalse
      (%==) SCJ SCJ = STrue
      (%==) SCJ SCK = SFalse
      (%==) SCJ SCL = SFalse
      (%==) SCJ SCM = SFalse
      (%==) SCJ SCN = SFalse
      (%==) SCJ SCO = SFalse
      (%==) SCJ SCP = SFalse
      (%==) SCJ SCQ = SFalse
      (%==) SCJ SCR = SFalse
      (%==) SCJ SCS = SFalse
      (%==) SCJ SCT = SFalse
      (%==) SCJ SCU = SFalse
      (%==) SCJ SCV = SFalse
      (%==) SCJ SCW = SFalse
      (%==) SCJ SCX = SFalse
      (%==) SCJ SCY = SFalse
      (%==) SCJ SCZ = SFalse
      (%==) SCK SCA = SFalse
      (%==) SCK SCB = SFalse
      (%==) SCK SCC = SFalse
      (%==) SCK SCD = SFalse
      (%==) SCK SCE = SFalse
      (%==) SCK SCF = SFalse
      (%==) SCK SCG = SFalse
      (%==) SCK SCH = SFalse
      (%==) SCK SCI = SFalse
      (%==) SCK SCJ = SFalse
      (%==) SCK SCK = STrue
      (%==) SCK SCL = SFalse
      (%==) SCK SCM = SFalse
      (%==) SCK SCN = SFalse
      (%==) SCK SCO = SFalse
      (%==) SCK SCP = SFalse
      (%==) SCK SCQ = SFalse
      (%==) SCK SCR = SFalse
      (%==) SCK SCS = SFalse
      (%==) SCK SCT = SFalse
      (%==) SCK SCU = SFalse
      (%==) SCK SCV = SFalse
      (%==) SCK SCW = SFalse
      (%==) SCK SCX = SFalse
      (%==) SCK SCY = SFalse
      (%==) SCK SCZ = SFalse
      (%==) SCL SCA = SFalse
      (%==) SCL SCB = SFalse
      (%==) SCL SCC = SFalse
      (%==) SCL SCD = SFalse
      (%==) SCL SCE = SFalse
      (%==) SCL SCF = SFalse
      (%==) SCL SCG = SFalse
      (%==) SCL SCH = SFalse
      (%==) SCL SCI = SFalse
      (%==) SCL SCJ = SFalse
      (%==) SCL SCK = SFalse
      (%==) SCL SCL = STrue
      (%==) SCL SCM = SFalse
      (%==) SCL SCN = SFalse
      (%==) SCL SCO = SFalse
      (%==) SCL SCP = SFalse
      (%==) SCL SCQ = SFalse
      (%==) SCL SCR = SFalse
      (%==) SCL SCS = SFalse
      (%==) SCL SCT = SFalse
      (%==) SCL SCU = SFalse
      (%==) SCL SCV = SFalse
      (%==) SCL SCW = SFalse
      (%==) SCL SCX = SFalse
      (%==) SCL SCY = SFalse
      (%==) SCL SCZ = SFalse
      (%==) SCM SCA = SFalse
      (%==) SCM SCB = SFalse
      (%==) SCM SCC = SFalse
      (%==) SCM SCD = SFalse
      (%==) SCM SCE = SFalse
      (%==) SCM SCF = SFalse
      (%==) SCM SCG = SFalse
      (%==) SCM SCH = SFalse
      (%==) SCM SCI = SFalse
      (%==) SCM SCJ = SFalse
      (%==) SCM SCK = SFalse
      (%==) SCM SCL = SFalse
      (%==) SCM SCM = STrue
      (%==) SCM SCN = SFalse
      (%==) SCM SCO = SFalse
      (%==) SCM SCP = SFalse
      (%==) SCM SCQ = SFalse
      (%==) SCM SCR = SFalse
      (%==) SCM SCS = SFalse
      (%==) SCM SCT = SFalse
      (%==) SCM SCU = SFalse
      (%==) SCM SCV = SFalse
      (%==) SCM SCW = SFalse
      (%==) SCM SCX = SFalse
      (%==) SCM SCY = SFalse
      (%==) SCM SCZ = SFalse
      (%==) SCN SCA = SFalse
      (%==) SCN SCB = SFalse
      (%==) SCN SCC = SFalse
      (%==) SCN SCD = SFalse
      (%==) SCN SCE = SFalse
      (%==) SCN SCF = SFalse
      (%==) SCN SCG = SFalse
      (%==) SCN SCH = SFalse
      (%==) SCN SCI = SFalse
      (%==) SCN SCJ = SFalse
      (%==) SCN SCK = SFalse
      (%==) SCN SCL = SFalse
      (%==) SCN SCM = SFalse
      (%==) SCN SCN = STrue
      (%==) SCN SCO = SFalse
      (%==) SCN SCP = SFalse
      (%==) SCN SCQ = SFalse
      (%==) SCN SCR = SFalse
      (%==) SCN SCS = SFalse
      (%==) SCN SCT = SFalse
      (%==) SCN SCU = SFalse
      (%==) SCN SCV = SFalse
      (%==) SCN SCW = SFalse
      (%==) SCN SCX = SFalse
      (%==) SCN SCY = SFalse
      (%==) SCN SCZ = SFalse
      (%==) SCO SCA = SFalse
      (%==) SCO SCB = SFalse
      (%==) SCO SCC = SFalse
      (%==) SCO SCD = SFalse
      (%==) SCO SCE = SFalse
      (%==) SCO SCF = SFalse
      (%==) SCO SCG = SFalse
      (%==) SCO SCH = SFalse
      (%==) SCO SCI = SFalse
      (%==) SCO SCJ = SFalse
      (%==) SCO SCK = SFalse
      (%==) SCO SCL = SFalse
      (%==) SCO SCM = SFalse
      (%==) SCO SCN = SFalse
      (%==) SCO SCO = STrue
      (%==) SCO SCP = SFalse
      (%==) SCO SCQ = SFalse
      (%==) SCO SCR = SFalse
      (%==) SCO SCS = SFalse
      (%==) SCO SCT = SFalse
      (%==) SCO SCU = SFalse
      (%==) SCO SCV = SFalse
      (%==) SCO SCW = SFalse
      (%==) SCO SCX = SFalse
      (%==) SCO SCY = SFalse
      (%==) SCO SCZ = SFalse
      (%==) SCP SCA = SFalse
      (%==) SCP SCB = SFalse
      (%==) SCP SCC = SFalse
      (%==) SCP SCD = SFalse
      (%==) SCP SCE = SFalse
      (%==) SCP SCF = SFalse
      (%==) SCP SCG = SFalse
      (%==) SCP SCH = SFalse
      (%==) SCP SCI = SFalse
      (%==) SCP SCJ = SFalse
      (%==) SCP SCK = SFalse
      (%==) SCP SCL = SFalse
      (%==) SCP SCM = SFalse
      (%==) SCP SCN = SFalse
      (%==) SCP SCO = SFalse
      (%==) SCP SCP = STrue
      (%==) SCP SCQ = SFalse
      (%==) SCP SCR = SFalse
      (%==) SCP SCS = SFalse
      (%==) SCP SCT = SFalse
      (%==) SCP SCU = SFalse
      (%==) SCP SCV = SFalse
      (%==) SCP SCW = SFalse
      (%==) SCP SCX = SFalse
      (%==) SCP SCY = SFalse
      (%==) SCP SCZ = SFalse
      (%==) SCQ SCA = SFalse
      (%==) SCQ SCB = SFalse
      (%==) SCQ SCC = SFalse
      (%==) SCQ SCD = SFalse
      (%==) SCQ SCE = SFalse
      (%==) SCQ SCF = SFalse
      (%==) SCQ SCG = SFalse
      (%==) SCQ SCH = SFalse
      (%==) SCQ SCI = SFalse
      (%==) SCQ SCJ = SFalse
      (%==) SCQ SCK = SFalse
      (%==) SCQ SCL = SFalse
      (%==) SCQ SCM = SFalse
      (%==) SCQ SCN = SFalse
      (%==) SCQ SCO = SFalse
      (%==) SCQ SCP = SFalse
      (%==) SCQ SCQ = STrue
      (%==) SCQ SCR = SFalse
      (%==) SCQ SCS = SFalse
      (%==) SCQ SCT = SFalse
      (%==) SCQ SCU = SFalse
      (%==) SCQ SCV = SFalse
      (%==) SCQ SCW = SFalse
      (%==) SCQ SCX = SFalse
      (%==) SCQ SCY = SFalse
      (%==) SCQ SCZ = SFalse
      (%==) SCR SCA = SFalse
      (%==) SCR SCB = SFalse
      (%==) SCR SCC = SFalse
      (%==) SCR SCD = SFalse
      (%==) SCR SCE = SFalse
      (%==) SCR SCF = SFalse
      (%==) SCR SCG = SFalse
      (%==) SCR SCH = SFalse
      (%==) SCR SCI = SFalse
      (%==) SCR SCJ = SFalse
      (%==) SCR SCK = SFalse
      (%==) SCR SCL = SFalse
      (%==) SCR SCM = SFalse
      (%==) SCR SCN = SFalse
      (%==) SCR SCO = SFalse
      (%==) SCR SCP = SFalse
      (%==) SCR SCQ = SFalse
      (%==) SCR SCR = STrue
      (%==) SCR SCS = SFalse
      (%==) SCR SCT = SFalse
      (%==) SCR SCU = SFalse
      (%==) SCR SCV = SFalse
      (%==) SCR SCW = SFalse
      (%==) SCR SCX = SFalse
      (%==) SCR SCY = SFalse
      (%==) SCR SCZ = SFalse
      (%==) SCS SCA = SFalse
      (%==) SCS SCB = SFalse
      (%==) SCS SCC = SFalse
      (%==) SCS SCD = SFalse
      (%==) SCS SCE = SFalse
      (%==) SCS SCF = SFalse
      (%==) SCS SCG = SFalse
      (%==) SCS SCH = SFalse
      (%==) SCS SCI = SFalse
      (%==) SCS SCJ = SFalse
      (%==) SCS SCK = SFalse
      (%==) SCS SCL = SFalse
      (%==) SCS SCM = SFalse
      (%==) SCS SCN = SFalse
      (%==) SCS SCO = SFalse
      (%==) SCS SCP = SFalse
      (%==) SCS SCQ = SFalse
      (%==) SCS SCR = SFalse
      (%==) SCS SCS = STrue
      (%==) SCS SCT = SFalse
      (%==) SCS SCU = SFalse
      (%==) SCS SCV = SFalse
      (%==) SCS SCW = SFalse
      (%==) SCS SCX = SFalse
      (%==) SCS SCY = SFalse
      (%==) SCS SCZ = SFalse
      (%==) SCT SCA = SFalse
      (%==) SCT SCB = SFalse
      (%==) SCT SCC = SFalse
      (%==) SCT SCD = SFalse
      (%==) SCT SCE = SFalse
      (%==) SCT SCF = SFalse
      (%==) SCT SCG = SFalse
      (%==) SCT SCH = SFalse
      (%==) SCT SCI = SFalse
      (%==) SCT SCJ = SFalse
      (%==) SCT SCK = SFalse
      (%==) SCT SCL = SFalse
      (%==) SCT SCM = SFalse
      (%==) SCT SCN = SFalse
      (%==) SCT SCO = SFalse
      (%==) SCT SCP = SFalse
      (%==) SCT SCQ = SFalse
      (%==) SCT SCR = SFalse
      (%==) SCT SCS = SFalse
      (%==) SCT SCT = STrue
      (%==) SCT SCU = SFalse
      (%==) SCT SCV = SFalse
      (%==) SCT SCW = SFalse
      (%==) SCT SCX = SFalse
      (%==) SCT SCY = SFalse
      (%==) SCT SCZ = SFalse
      (%==) SCU SCA = SFalse
      (%==) SCU SCB = SFalse
      (%==) SCU SCC = SFalse
      (%==) SCU SCD = SFalse
      (%==) SCU SCE = SFalse
      (%==) SCU SCF = SFalse
      (%==) SCU SCG = SFalse
      (%==) SCU SCH = SFalse
      (%==) SCU SCI = SFalse
      (%==) SCU SCJ = SFalse
      (%==) SCU SCK = SFalse
      (%==) SCU SCL = SFalse
      (%==) SCU SCM = SFalse
      (%==) SCU SCN = SFalse
      (%==) SCU SCO = SFalse
      (%==) SCU SCP = SFalse
      (%==) SCU SCQ = SFalse
      (%==) SCU SCR = SFalse
      (%==) SCU SCS = SFalse
      (%==) SCU SCT = SFalse
      (%==) SCU SCU = STrue
      (%==) SCU SCV = SFalse
      (%==) SCU SCW = SFalse
      (%==) SCU SCX = SFalse
      (%==) SCU SCY = SFalse
      (%==) SCU SCZ = SFalse
      (%==) SCV SCA = SFalse
      (%==) SCV SCB = SFalse
      (%==) SCV SCC = SFalse
      (%==) SCV SCD = SFalse
      (%==) SCV SCE = SFalse
      (%==) SCV SCF = SFalse
      (%==) SCV SCG = SFalse
      (%==) SCV SCH = SFalse
      (%==) SCV SCI = SFalse
      (%==) SCV SCJ = SFalse
      (%==) SCV SCK = SFalse
      (%==) SCV SCL = SFalse
      (%==) SCV SCM = SFalse
      (%==) SCV SCN = SFalse
      (%==) SCV SCO = SFalse
      (%==) SCV SCP = SFalse
      (%==) SCV SCQ = SFalse
      (%==) SCV SCR = SFalse
      (%==) SCV SCS = SFalse
      (%==) SCV SCT = SFalse
      (%==) SCV SCU = SFalse
      (%==) SCV SCV = STrue
      (%==) SCV SCW = SFalse
      (%==) SCV SCX = SFalse
      (%==) SCV SCY = SFalse
      (%==) SCV SCZ = SFalse
      (%==) SCW SCA = SFalse
      (%==) SCW SCB = SFalse
      (%==) SCW SCC = SFalse
      (%==) SCW SCD = SFalse
      (%==) SCW SCE = SFalse
      (%==) SCW SCF = SFalse
      (%==) SCW SCG = SFalse
      (%==) SCW SCH = SFalse
      (%==) SCW SCI = SFalse
      (%==) SCW SCJ = SFalse
      (%==) SCW SCK = SFalse
      (%==) SCW SCL = SFalse
      (%==) SCW SCM = SFalse
      (%==) SCW SCN = SFalse
      (%==) SCW SCO = SFalse
      (%==) SCW SCP = SFalse
      (%==) SCW SCQ = SFalse
      (%==) SCW SCR = SFalse
      (%==) SCW SCS = SFalse
      (%==) SCW SCT = SFalse
      (%==) SCW SCU = SFalse
      (%==) SCW SCV = SFalse
      (%==) SCW SCW = STrue
      (%==) SCW SCX = SFalse
      (%==) SCW SCY = SFalse
      (%==) SCW SCZ = SFalse
      (%==) SCX SCA = SFalse
      (%==) SCX SCB = SFalse
      (%==) SCX SCC = SFalse
      (%==) SCX SCD = SFalse
      (%==) SCX SCE = SFalse
      (%==) SCX SCF = SFalse
      (%==) SCX SCG = SFalse
      (%==) SCX SCH = SFalse
      (%==) SCX SCI = SFalse
      (%==) SCX SCJ = SFalse
      (%==) SCX SCK = SFalse
      (%==) SCX SCL = SFalse
      (%==) SCX SCM = SFalse
      (%==) SCX SCN = SFalse
      (%==) SCX SCO = SFalse
      (%==) SCX SCP = SFalse
      (%==) SCX SCQ = SFalse
      (%==) SCX SCR = SFalse
      (%==) SCX SCS = SFalse
      (%==) SCX SCT = SFalse
      (%==) SCX SCU = SFalse
      (%==) SCX SCV = SFalse
      (%==) SCX SCW = SFalse
      (%==) SCX SCX = STrue
      (%==) SCX SCY = SFalse
      (%==) SCX SCZ = SFalse
      (%==) SCY SCA = SFalse
      (%==) SCY SCB = SFalse
      (%==) SCY SCC = SFalse
      (%==) SCY SCD = SFalse
      (%==) SCY SCE = SFalse
      (%==) SCY SCF = SFalse
      (%==) SCY SCG = SFalse
      (%==) SCY SCH = SFalse
      (%==) SCY SCI = SFalse
      (%==) SCY SCJ = SFalse
      (%==) SCY SCK = SFalse
      (%==) SCY SCL = SFalse
      (%==) SCY SCM = SFalse
      (%==) SCY SCN = SFalse
      (%==) SCY SCO = SFalse
      (%==) SCY SCP = SFalse
      (%==) SCY SCQ = SFalse
      (%==) SCY SCR = SFalse
      (%==) SCY SCS = SFalse
      (%==) SCY SCT = SFalse
      (%==) SCY SCU = SFalse
      (%==) SCY SCV = SFalse
      (%==) SCY SCW = SFalse
      (%==) SCY SCX = SFalse
      (%==) SCY SCY = STrue
      (%==) SCY SCZ = SFalse
      (%==) SCZ SCA = SFalse
      (%==) SCZ SCB = SFalse
      (%==) SCZ SCC = SFalse
      (%==) SCZ SCD = SFalse
      (%==) SCZ SCE = SFalse
      (%==) SCZ SCF = SFalse
      (%==) SCZ SCG = SFalse
      (%==) SCZ SCH = SFalse
      (%==) SCZ SCI = SFalse
      (%==) SCZ SCJ = SFalse
      (%==) SCZ SCK = SFalse
      (%==) SCZ SCL = SFalse
      (%==) SCZ SCM = SFalse
      (%==) SCZ SCN = SFalse
      (%==) SCZ SCO = SFalse
      (%==) SCZ SCP = SFalse
      (%==) SCZ SCQ = SFalse
      (%==) SCZ SCR = SFalse
      (%==) SCZ SCS = SFalse
      (%==) SCZ SCT = SFalse
      (%==) SCZ SCU = SFalse
      (%==) SCZ SCV = SFalse
      (%==) SCZ SCW = SFalse
      (%==) SCZ SCX = SFalse
      (%==) SCZ SCY = SFalse
      (%==) SCZ SCZ = STrue
    instance SDecide AChar where
      (%~) SCA SCA = Proved Refl
      (%~) SCA SCB = Disproved (\ x -> case x of)
      (%~) SCA SCC = Disproved (\ x -> case x of)
      (%~) SCA SCD = Disproved (\ x -> case x of)
      (%~) SCA SCE = Disproved (\ x -> case x of)
      (%~) SCA SCF = Disproved (\ x -> case x of)
      (%~) SCA SCG = Disproved (\ x -> case x of)
      (%~) SCA SCH = Disproved (\ x -> case x of)
      (%~) SCA SCI = Disproved (\ x -> case x of)
      (%~) SCA SCJ = Disproved (\ x -> case x of)
      (%~) SCA SCK = Disproved (\ x -> case x of)
      (%~) SCA SCL = Disproved (\ x -> case x of)
      (%~) SCA SCM = Disproved (\ x -> case x of)
      (%~) SCA SCN = Disproved (\ x -> case x of)
      (%~) SCA SCO = Disproved (\ x -> case x of)
      (%~) SCA SCP = Disproved (\ x -> case x of)
      (%~) SCA SCQ = Disproved (\ x -> case x of)
      (%~) SCA SCR = Disproved (\ x -> case x of)
      (%~) SCA SCS = Disproved (\ x -> case x of)
      (%~) SCA SCT = Disproved (\ x -> case x of)
      (%~) SCA SCU = Disproved (\ x -> case x of)
      (%~) SCA SCV = Disproved (\ x -> case x of)
      (%~) SCA SCW = Disproved (\ x -> case x of)
      (%~) SCA SCX = Disproved (\ x -> case x of)
      (%~) SCA SCY = Disproved (\ x -> case x of)
      (%~) SCA SCZ = Disproved (\ x -> case x of)
      (%~) SCB SCA = Disproved (\ x -> case x of)
      (%~) SCB SCB = Proved Refl
      (%~) SCB SCC = Disproved (\ x -> case x of)
      (%~) SCB SCD = Disproved (\ x -> case x of)
      (%~) SCB SCE = Disproved (\ x -> case x of)
      (%~) SCB SCF = Disproved (\ x -> case x of)
      (%~) SCB SCG = Disproved (\ x -> case x of)
      (%~) SCB SCH = Disproved (\ x -> case x of)
      (%~) SCB SCI = Disproved (\ x -> case x of)
      (%~) SCB SCJ = Disproved (\ x -> case x of)
      (%~) SCB SCK = Disproved (\ x -> case x of)
      (%~) SCB SCL = Disproved (\ x -> case x of)
      (%~) SCB SCM = Disproved (\ x -> case x of)
      (%~) SCB SCN = Disproved (\ x -> case x of)
      (%~) SCB SCO = Disproved (\ x -> case x of)
      (%~) SCB SCP = Disproved (\ x -> case x of)
      (%~) SCB SCQ = Disproved (\ x -> case x of)
      (%~) SCB SCR = Disproved (\ x -> case x of)
      (%~) SCB SCS = Disproved (\ x -> case x of)
      (%~) SCB SCT = Disproved (\ x -> case x of)
      (%~) SCB SCU = Disproved (\ x -> case x of)
      (%~) SCB SCV = Disproved (\ x -> case x of)
      (%~) SCB SCW = Disproved (\ x -> case x of)
      (%~) SCB SCX = Disproved (\ x -> case x of)
      (%~) SCB SCY = Disproved (\ x -> case x of)
      (%~) SCB SCZ = Disproved (\ x -> case x of)
      (%~) SCC SCA = Disproved (\ x -> case x of)
      (%~) SCC SCB = Disproved (\ x -> case x of)
      (%~) SCC SCC = Proved Refl
      (%~) SCC SCD = Disproved (\ x -> case x of)
      (%~) SCC SCE = Disproved (\ x -> case x of)
      (%~) SCC SCF = Disproved (\ x -> case x of)
      (%~) SCC SCG = Disproved (\ x -> case x of)
      (%~) SCC SCH = Disproved (\ x -> case x of)
      (%~) SCC SCI = Disproved (\ x -> case x of)
      (%~) SCC SCJ = Disproved (\ x -> case x of)
      (%~) SCC SCK = Disproved (\ x -> case x of)
      (%~) SCC SCL = Disproved (\ x -> case x of)
      (%~) SCC SCM = Disproved (\ x -> case x of)
      (%~) SCC SCN = Disproved (\ x -> case x of)
      (%~) SCC SCO = Disproved (\ x -> case x of)
      (%~) SCC SCP = Disproved (\ x -> case x of)
      (%~) SCC SCQ = Disproved (\ x -> case x of)
      (%~) SCC SCR = Disproved (\ x -> case x of)
      (%~) SCC SCS = Disproved (\ x -> case x of)
      (%~) SCC SCT = Disproved (\ x -> case x of)
      (%~) SCC SCU = Disproved (\ x -> case x of)
      (%~) SCC SCV = Disproved (\ x -> case x of)
      (%~) SCC SCW = Disproved (\ x -> case x of)
      (%~) SCC SCX = Disproved (\ x -> case x of)
      (%~) SCC SCY = Disproved (\ x -> case x of)
      (%~) SCC SCZ = Disproved (\ x -> case x of)
      (%~) SCD SCA = Disproved (\ x -> case x of)
      (%~) SCD SCB = Disproved (\ x -> case x of)
      (%~) SCD SCC = Disproved (\ x -> case x of)
      (%~) SCD SCD = Proved Refl
      (%~) SCD SCE = Disproved (\ x -> case x of)
      (%~) SCD SCF = Disproved (\ x -> case x of)
      (%~) SCD SCG = Disproved (\ x -> case x of)
      (%~) SCD SCH = Disproved (\ x -> case x of)
      (%~) SCD SCI = Disproved (\ x -> case x of)
      (%~) SCD SCJ = Disproved (\ x -> case x of)
      (%~) SCD SCK = Disproved (\ x -> case x of)
      (%~) SCD SCL = Disproved (\ x -> case x of)
      (%~) SCD SCM = Disproved (\ x -> case x of)
      (%~) SCD SCN = Disproved (\ x -> case x of)
      (%~) SCD SCO = Disproved (\ x -> case x of)
      (%~) SCD SCP = Disproved (\ x -> case x of)
      (%~) SCD SCQ = Disproved (\ x -> case x of)
      (%~) SCD SCR = Disproved (\ x -> case x of)
      (%~) SCD SCS = Disproved (\ x -> case x of)
      (%~) SCD SCT = Disproved (\ x -> case x of)
      (%~) SCD SCU = Disproved (\ x -> case x of)
      (%~) SCD SCV = Disproved (\ x -> case x of)
      (%~) SCD SCW = Disproved (\ x -> case x of)
      (%~) SCD SCX = Disproved (\ x -> case x of)
      (%~) SCD SCY = Disproved (\ x -> case x of)
      (%~) SCD SCZ = Disproved (\ x -> case x of)
      (%~) SCE SCA = Disproved (\ x -> case x of)
      (%~) SCE SCB = Disproved (\ x -> case x of)
      (%~) SCE SCC = Disproved (\ x -> case x of)
      (%~) SCE SCD = Disproved (\ x -> case x of)
      (%~) SCE SCE = Proved Refl
      (%~) SCE SCF = Disproved (\ x -> case x of)
      (%~) SCE SCG = Disproved (\ x -> case x of)
      (%~) SCE SCH = Disproved (\ x -> case x of)
      (%~) SCE SCI = Disproved (\ x -> case x of)
      (%~) SCE SCJ = Disproved (\ x -> case x of)
      (%~) SCE SCK = Disproved (\ x -> case x of)
      (%~) SCE SCL = Disproved (\ x -> case x of)
      (%~) SCE SCM = Disproved (\ x -> case x of)
      (%~) SCE SCN = Disproved (\ x -> case x of)
      (%~) SCE SCO = Disproved (\ x -> case x of)
      (%~) SCE SCP = Disproved (\ x -> case x of)
      (%~) SCE SCQ = Disproved (\ x -> case x of)
      (%~) SCE SCR = Disproved (\ x -> case x of)
      (%~) SCE SCS = Disproved (\ x -> case x of)
      (%~) SCE SCT = Disproved (\ x -> case x of)
      (%~) SCE SCU = Disproved (\ x -> case x of)
      (%~) SCE SCV = Disproved (\ x -> case x of)
      (%~) SCE SCW = Disproved (\ x -> case x of)
      (%~) SCE SCX = Disproved (\ x -> case x of)
      (%~) SCE SCY = Disproved (\ x -> case x of)
      (%~) SCE SCZ = Disproved (\ x -> case x of)
      (%~) SCF SCA = Disproved (\ x -> case x of)
      (%~) SCF SCB = Disproved (\ x -> case x of)
      (%~) SCF SCC = Disproved (\ x -> case x of)
      (%~) SCF SCD = Disproved (\ x -> case x of)
      (%~) SCF SCE = Disproved (\ x -> case x of)
      (%~) SCF SCF = Proved Refl
      (%~) SCF SCG = Disproved (\ x -> case x of)
      (%~) SCF SCH = Disproved (\ x -> case x of)
      (%~) SCF SCI = Disproved (\ x -> case x of)
      (%~) SCF SCJ = Disproved (\ x -> case x of)
      (%~) SCF SCK = Disproved (\ x -> case x of)
      (%~) SCF SCL = Disproved (\ x -> case x of)
      (%~) SCF SCM = Disproved (\ x -> case x of)
      (%~) SCF SCN = Disproved (\ x -> case x of)
      (%~) SCF SCO = Disproved (\ x -> case x of)
      (%~) SCF SCP = Disproved (\ x -> case x of)
      (%~) SCF SCQ = Disproved (\ x -> case x of)
      (%~) SCF SCR = Disproved (\ x -> case x of)
      (%~) SCF SCS = Disproved (\ x -> case x of)
      (%~) SCF SCT = Disproved (\ x -> case x of)
      (%~) SCF SCU = Disproved (\ x -> case x of)
      (%~) SCF SCV = Disproved (\ x -> case x of)
      (%~) SCF SCW = Disproved (\ x -> case x of)
      (%~) SCF SCX = Disproved (\ x -> case x of)
      (%~) SCF SCY = Disproved (\ x -> case x of)
      (%~) SCF SCZ = Disproved (\ x -> case x of)
      (%~) SCG SCA = Disproved (\ x -> case x of)
      (%~) SCG SCB = Disproved (\ x -> case x of)
      (%~) SCG SCC = Disproved (\ x -> case x of)
      (%~) SCG SCD = Disproved (\ x -> case x of)
      (%~) SCG SCE = Disproved (\ x -> case x of)
      (%~) SCG SCF = Disproved (\ x -> case x of)
      (%~) SCG SCG = Proved Refl
      (%~) SCG SCH = Disproved (\ x -> case x of)
      (%~) SCG SCI = Disproved (\ x -> case x of)
      (%~) SCG SCJ = Disproved (\ x -> case x of)
      (%~) SCG SCK = Disproved (\ x -> case x of)
      (%~) SCG SCL = Disproved (\ x -> case x of)
      (%~) SCG SCM = Disproved (\ x -> case x of)
      (%~) SCG SCN = Disproved (\ x -> case x of)
      (%~) SCG SCO = Disproved (\ x -> case x of)
      (%~) SCG SCP = Disproved (\ x -> case x of)
      (%~) SCG SCQ = Disproved (\ x -> case x of)
      (%~) SCG SCR = Disproved (\ x -> case x of)
      (%~) SCG SCS = Disproved (\ x -> case x of)
      (%~) SCG SCT = Disproved (\ x -> case x of)
      (%~) SCG SCU = Disproved (\ x -> case x of)
      (%~) SCG SCV = Disproved (\ x -> case x of)
      (%~) SCG SCW = Disproved (\ x -> case x of)
      (%~) SCG SCX = Disproved (\ x -> case x of)
      (%~) SCG SCY = Disproved (\ x -> case x of)
      (%~) SCG SCZ = Disproved (\ x -> case x of)
      (%~) SCH SCA = Disproved (\ x -> case x of)
      (%~) SCH SCB = Disproved (\ x -> case x of)
      (%~) SCH SCC = Disproved (\ x -> case x of)
      (%~) SCH SCD = Disproved (\ x -> case x of)
      (%~) SCH SCE = Disproved (\ x -> case x of)
      (%~) SCH SCF = Disproved (\ x -> case x of)
      (%~) SCH SCG = Disproved (\ x -> case x of)
      (%~) SCH SCH = Proved Refl
      (%~) SCH SCI = Disproved (\ x -> case x of)
      (%~) SCH SCJ = Disproved (\ x -> case x of)
      (%~) SCH SCK = Disproved (\ x -> case x of)
      (%~) SCH SCL = Disproved (\ x -> case x of)
      (%~) SCH SCM = Disproved (\ x -> case x of)
      (%~) SCH SCN = Disproved (\ x -> case x of)
      (%~) SCH SCO = Disproved (\ x -> case x of)
      (%~) SCH SCP = Disproved (\ x -> case x of)
      (%~) SCH SCQ = Disproved (\ x -> case x of)
      (%~) SCH SCR = Disproved (\ x -> case x of)
      (%~) SCH SCS = Disproved (\ x -> case x of)
      (%~) SCH SCT = Disproved (\ x -> case x of)
      (%~) SCH SCU = Disproved (\ x -> case x of)
      (%~) SCH SCV = Disproved (\ x -> case x of)
      (%~) SCH SCW = Disproved (\ x -> case x of)
      (%~) SCH SCX = Disproved (\ x -> case x of)
      (%~) SCH SCY = Disproved (\ x -> case x of)
      (%~) SCH SCZ = Disproved (\ x -> case x of)
      (%~) SCI SCA = Disproved (\ x -> case x of)
      (%~) SCI SCB = Disproved (\ x -> case x of)
      (%~) SCI SCC = Disproved (\ x -> case x of)
      (%~) SCI SCD = Disproved (\ x -> case x of)
      (%~) SCI SCE = Disproved (\ x -> case x of)
      (%~) SCI SCF = Disproved (\ x -> case x of)
      (%~) SCI SCG = Disproved (\ x -> case x of)
      (%~) SCI SCH = Disproved (\ x -> case x of)
      (%~) SCI SCI = Proved Refl
      (%~) SCI SCJ = Disproved (\ x -> case x of)
      (%~) SCI SCK = Disproved (\ x -> case x of)
      (%~) SCI SCL = Disproved (\ x -> case x of)
      (%~) SCI SCM = Disproved (\ x -> case x of)
      (%~) SCI SCN = Disproved (\ x -> case x of)
      (%~) SCI SCO = Disproved (\ x -> case x of)
      (%~) SCI SCP = Disproved (\ x -> case x of)
      (%~) SCI SCQ = Disproved (\ x -> case x of)
      (%~) SCI SCR = Disproved (\ x -> case x of)
      (%~) SCI SCS = Disproved (\ x -> case x of)
      (%~) SCI SCT = Disproved (\ x -> case x of)
      (%~) SCI SCU = Disproved (\ x -> case x of)
      (%~) SCI SCV = Disproved (\ x -> case x of)
      (%~) SCI SCW = Disproved (\ x -> case x of)
      (%~) SCI SCX = Disproved (\ x -> case x of)
      (%~) SCI SCY = Disproved (\ x -> case x of)
      (%~) SCI SCZ = Disproved (\ x -> case x of)
      (%~) SCJ SCA = Disproved (\ x -> case x of)
      (%~) SCJ SCB = Disproved (\ x -> case x of)
      (%~) SCJ SCC = Disproved (\ x -> case x of)
      (%~) SCJ SCD = Disproved (\ x -> case x of)
      (%~) SCJ SCE = Disproved (\ x -> case x of)
      (%~) SCJ SCF = Disproved (\ x -> case x of)
      (%~) SCJ SCG = Disproved (\ x -> case x of)
      (%~) SCJ SCH = Disproved (\ x -> case x of)
      (%~) SCJ SCI = Disproved (\ x -> case x of)
      (%~) SCJ SCJ = Proved Refl
      (%~) SCJ SCK = Disproved (\ x -> case x of)
      (%~) SCJ SCL = Disproved (\ x -> case x of)
      (%~) SCJ SCM = Disproved (\ x -> case x of)
      (%~) SCJ SCN = Disproved (\ x -> case x of)
      (%~) SCJ SCO = Disproved (\ x -> case x of)
      (%~) SCJ SCP = Disproved (\ x -> case x of)
      (%~) SCJ SCQ = Disproved (\ x -> case x of)
      (%~) SCJ SCR = Disproved (\ x -> case x of)
      (%~) SCJ SCS = Disproved (\ x -> case x of)
      (%~) SCJ SCT = Disproved (\ x -> case x of)
      (%~) SCJ SCU = Disproved (\ x -> case x of)
      (%~) SCJ SCV = Disproved (\ x -> case x of)
      (%~) SCJ SCW = Disproved (\ x -> case x of)
      (%~) SCJ SCX = Disproved (\ x -> case x of)
      (%~) SCJ SCY = Disproved (\ x -> case x of)
      (%~) SCJ SCZ = Disproved (\ x -> case x of)
      (%~) SCK SCA = Disproved (\ x -> case x of)
      (%~) SCK SCB = Disproved (\ x -> case x of)
      (%~) SCK SCC = Disproved (\ x -> case x of)
      (%~) SCK SCD = Disproved (\ x -> case x of)
      (%~) SCK SCE = Disproved (\ x -> case x of)
      (%~) SCK SCF = Disproved (\ x -> case x of)
      (%~) SCK SCG = Disproved (\ x -> case x of)
      (%~) SCK SCH = Disproved (\ x -> case x of)
      (%~) SCK SCI = Disproved (\ x -> case x of)
      (%~) SCK SCJ = Disproved (\ x -> case x of)
      (%~) SCK SCK = Proved Refl
      (%~) SCK SCL = Disproved (\ x -> case x of)
      (%~) SCK SCM = Disproved (\ x -> case x of)
      (%~) SCK SCN = Disproved (\ x -> case x of)
      (%~) SCK SCO = Disproved (\ x -> case x of)
      (%~) SCK SCP = Disproved (\ x -> case x of)
      (%~) SCK SCQ = Disproved (\ x -> case x of)
      (%~) SCK SCR = Disproved (\ x -> case x of)
      (%~) SCK SCS = Disproved (\ x -> case x of)
      (%~) SCK SCT = Disproved (\ x -> case x of)
      (%~) SCK SCU = Disproved (\ x -> case x of)
      (%~) SCK SCV = Disproved (\ x -> case x of)
      (%~) SCK SCW = Disproved (\ x -> case x of)
      (%~) SCK SCX = Disproved (\ x -> case x of)
      (%~) SCK SCY = Disproved (\ x -> case x of)
      (%~) SCK SCZ = Disproved (\ x -> case x of)
      (%~) SCL SCA = Disproved (\ x -> case x of)
      (%~) SCL SCB = Disproved (\ x -> case x of)
      (%~) SCL SCC = Disproved (\ x -> case x of)
      (%~) SCL SCD = Disproved (\ x -> case x of)
      (%~) SCL SCE = Disproved (\ x -> case x of)
      (%~) SCL SCF = Disproved (\ x -> case x of)
      (%~) SCL SCG = Disproved (\ x -> case x of)
      (%~) SCL SCH = Disproved (\ x -> case x of)
      (%~) SCL SCI = Disproved (\ x -> case x of)
      (%~) SCL SCJ = Disproved (\ x -> case x of)
      (%~) SCL SCK = Disproved (\ x -> case x of)
      (%~) SCL SCL = Proved Refl
      (%~) SCL SCM = Disproved (\ x -> case x of)
      (%~) SCL SCN = Disproved (\ x -> case x of)
      (%~) SCL SCO = Disproved (\ x -> case x of)
      (%~) SCL SCP = Disproved (\ x -> case x of)
      (%~) SCL SCQ = Disproved (\ x -> case x of)
      (%~) SCL SCR = Disproved (\ x -> case x of)
      (%~) SCL SCS = Disproved (\ x -> case x of)
      (%~) SCL SCT = Disproved (\ x -> case x of)
      (%~) SCL SCU = Disproved (\ x -> case x of)
      (%~) SCL SCV = Disproved (\ x -> case x of)
      (%~) SCL SCW = Disproved (\ x -> case x of)
      (%~) SCL SCX = Disproved (\ x -> case x of)
      (%~) SCL SCY = Disproved (\ x -> case x of)
      (%~) SCL SCZ = Disproved (\ x -> case x of)
      (%~) SCM SCA = Disproved (\ x -> case x of)
      (%~) SCM SCB = Disproved (\ x -> case x of)
      (%~) SCM SCC = Disproved (\ x -> case x of)
      (%~) SCM SCD = Disproved (\ x -> case x of)
      (%~) SCM SCE = Disproved (\ x -> case x of)
      (%~) SCM SCF = Disproved (\ x -> case x of)
      (%~) SCM SCG = Disproved (\ x -> case x of)
      (%~) SCM SCH = Disproved (\ x -> case x of)
      (%~) SCM SCI = Disproved (\ x -> case x of)
      (%~) SCM SCJ = Disproved (\ x -> case x of)
      (%~) SCM SCK = Disproved (\ x -> case x of)
      (%~) SCM SCL = Disproved (\ x -> case x of)
      (%~) SCM SCM = Proved Refl
      (%~) SCM SCN = Disproved (\ x -> case x of)
      (%~) SCM SCO = Disproved (\ x -> case x of)
      (%~) SCM SCP = Disproved (\ x -> case x of)
      (%~) SCM SCQ = Disproved (\ x -> case x of)
      (%~) SCM SCR = Disproved (\ x -> case x of)
      (%~) SCM SCS = Disproved (\ x -> case x of)
      (%~) SCM SCT = Disproved (\ x -> case x of)
      (%~) SCM SCU = Disproved (\ x -> case x of)
      (%~) SCM SCV = Disproved (\ x -> case x of)
      (%~) SCM SCW = Disproved (\ x -> case x of)
      (%~) SCM SCX = Disproved (\ x -> case x of)
      (%~) SCM SCY = Disproved (\ x -> case x of)
      (%~) SCM SCZ = Disproved (\ x -> case x of)
      (%~) SCN SCA = Disproved (\ x -> case x of)
      (%~) SCN SCB = Disproved (\ x -> case x of)
      (%~) SCN SCC = Disproved (\ x -> case x of)
      (%~) SCN SCD = Disproved (\ x -> case x of)
      (%~) SCN SCE = Disproved (\ x -> case x of)
      (%~) SCN SCF = Disproved (\ x -> case x of)
      (%~) SCN SCG = Disproved (\ x -> case x of)
      (%~) SCN SCH = Disproved (\ x -> case x of)
      (%~) SCN SCI = Disproved (\ x -> case x of)
      (%~) SCN SCJ = Disproved (\ x -> case x of)
      (%~) SCN SCK = Disproved (\ x -> case x of)
      (%~) SCN SCL = Disproved (\ x -> case x of)
      (%~) SCN SCM = Disproved (\ x -> case x of)
      (%~) SCN SCN = Proved Refl
      (%~) SCN SCO = Disproved (\ x -> case x of)
      (%~) SCN SCP = Disproved (\ x -> case x of)
      (%~) SCN SCQ = Disproved (\ x -> case x of)
      (%~) SCN SCR = Disproved (\ x -> case x of)
      (%~) SCN SCS = Disproved (\ x -> case x of)
      (%~) SCN SCT = Disproved (\ x -> case x of)
      (%~) SCN SCU = Disproved (\ x -> case x of)
      (%~) SCN SCV = Disproved (\ x -> case x of)
      (%~) SCN SCW = Disproved (\ x -> case x of)
      (%~) SCN SCX = Disproved (\ x -> case x of)
      (%~) SCN SCY = Disproved (\ x -> case x of)
      (%~) SCN SCZ = Disproved (\ x -> case x of)
      (%~) SCO SCA = Disproved (\ x -> case x of)
      (%~) SCO SCB = Disproved (\ x -> case x of)
      (%~) SCO SCC = Disproved (\ x -> case x of)
      (%~) SCO SCD = Disproved (\ x -> case x of)
      (%~) SCO SCE = Disproved (\ x -> case x of)
      (%~) SCO SCF = Disproved (\ x -> case x of)
      (%~) SCO SCG = Disproved (\ x -> case x of)
      (%~) SCO SCH = Disproved (\ x -> case x of)
      (%~) SCO SCI = Disproved (\ x -> case x of)
      (%~) SCO SCJ = Disproved (\ x -> case x of)
      (%~) SCO SCK = Disproved (\ x -> case x of)
      (%~) SCO SCL = Disproved (\ x -> case x of)
      (%~) SCO SCM = Disproved (\ x -> case x of)
      (%~) SCO SCN = Disproved (\ x -> case x of)
      (%~) SCO SCO = Proved Refl
      (%~) SCO SCP = Disproved (\ x -> case x of)
      (%~) SCO SCQ = Disproved (\ x -> case x of)
      (%~) SCO SCR = Disproved (\ x -> case x of)
      (%~) SCO SCS = Disproved (\ x -> case x of)
      (%~) SCO SCT = Disproved (\ x -> case x of)
      (%~) SCO SCU = Disproved (\ x -> case x of)
      (%~) SCO SCV = Disproved (\ x -> case x of)
      (%~) SCO SCW = Disproved (\ x -> case x of)
      (%~) SCO SCX = Disproved (\ x -> case x of)
      (%~) SCO SCY = Disproved (\ x -> case x of)
      (%~) SCO SCZ = Disproved (\ x -> case x of)
      (%~) SCP SCA = Disproved (\ x -> case x of)
      (%~) SCP SCB = Disproved (\ x -> case x of)
      (%~) SCP SCC = Disproved (\ x -> case x of)
      (%~) SCP SCD = Disproved (\ x -> case x of)
      (%~) SCP SCE = Disproved (\ x -> case x of)
      (%~) SCP SCF = Disproved (\ x -> case x of)
      (%~) SCP SCG = Disproved (\ x -> case x of)
      (%~) SCP SCH = Disproved (\ x -> case x of)
      (%~) SCP SCI = Disproved (\ x -> case x of)
      (%~) SCP SCJ = Disproved (\ x -> case x of)
      (%~) SCP SCK = Disproved (\ x -> case x of)
      (%~) SCP SCL = Disproved (\ x -> case x of)
      (%~) SCP SCM = Disproved (\ x -> case x of)
      (%~) SCP SCN = Disproved (\ x -> case x of)
      (%~) SCP SCO = Disproved (\ x -> case x of)
      (%~) SCP SCP = Proved Refl
      (%~) SCP SCQ = Disproved (\ x -> case x of)
      (%~) SCP SCR = Disproved (\ x -> case x of)
      (%~) SCP SCS = Disproved (\ x -> case x of)
      (%~) SCP SCT = Disproved (\ x -> case x of)
      (%~) SCP SCU = Disproved (\ x -> case x of)
      (%~) SCP SCV = Disproved (\ x -> case x of)
      (%~) SCP SCW = Disproved (\ x -> case x of)
      (%~) SCP SCX = Disproved (\ x -> case x of)
      (%~) SCP SCY = Disproved (\ x -> case x of)
      (%~) SCP SCZ = Disproved (\ x -> case x of)
      (%~) SCQ SCA = Disproved (\ x -> case x of)
      (%~) SCQ SCB = Disproved (\ x -> case x of)
      (%~) SCQ SCC = Disproved (\ x -> case x of)
      (%~) SCQ SCD = Disproved (\ x -> case x of)
      (%~) SCQ SCE = Disproved (\ x -> case x of)
      (%~) SCQ SCF = Disproved (\ x -> case x of)
      (%~) SCQ SCG = Disproved (\ x -> case x of)
      (%~) SCQ SCH = Disproved (\ x -> case x of)
      (%~) SCQ SCI = Disproved (\ x -> case x of)
      (%~) SCQ SCJ = Disproved (\ x -> case x of)
      (%~) SCQ SCK = Disproved (\ x -> case x of)
      (%~) SCQ SCL = Disproved (\ x -> case x of)
      (%~) SCQ SCM = Disproved (\ x -> case x of)
      (%~) SCQ SCN = Disproved (\ x -> case x of)
      (%~) SCQ SCO = Disproved (\ x -> case x of)
      (%~) SCQ SCP = Disproved (\ x -> case x of)
      (%~) SCQ SCQ = Proved Refl
      (%~) SCQ SCR = Disproved (\ x -> case x of)
      (%~) SCQ SCS = Disproved (\ x -> case x of)
      (%~) SCQ SCT = Disproved (\ x -> case x of)
      (%~) SCQ SCU = Disproved (\ x -> case x of)
      (%~) SCQ SCV = Disproved (\ x -> case x of)
      (%~) SCQ SCW = Disproved (\ x -> case x of)
      (%~) SCQ SCX = Disproved (\ x -> case x of)
      (%~) SCQ SCY = Disproved (\ x -> case x of)
      (%~) SCQ SCZ = Disproved (\ x -> case x of)
      (%~) SCR SCA = Disproved (\ x -> case x of)
      (%~) SCR SCB = Disproved (\ x -> case x of)
      (%~) SCR SCC = Disproved (\ x -> case x of)
      (%~) SCR SCD = Disproved (\ x -> case x of)
      (%~) SCR SCE = Disproved (\ x -> case x of)
      (%~) SCR SCF = Disproved (\ x -> case x of)
      (%~) SCR SCG = Disproved (\ x -> case x of)
      (%~) SCR SCH = Disproved (\ x -> case x of)
      (%~) SCR SCI = Disproved (\ x -> case x of)
      (%~) SCR SCJ = Disproved (\ x -> case x of)
      (%~) SCR SCK = Disproved (\ x -> case x of)
      (%~) SCR SCL = Disproved (\ x -> case x of)
      (%~) SCR SCM = Disproved (\ x -> case x of)
      (%~) SCR SCN = Disproved (\ x -> case x of)
      (%~) SCR SCO = Disproved (\ x -> case x of)
      (%~) SCR SCP = Disproved (\ x -> case x of)
      (%~) SCR SCQ = Disproved (\ x -> case x of)
      (%~) SCR SCR = Proved Refl
      (%~) SCR SCS = Disproved (\ x -> case x of)
      (%~) SCR SCT = Disproved (\ x -> case x of)
      (%~) SCR SCU = Disproved (\ x -> case x of)
      (%~) SCR SCV = Disproved (\ x -> case x of)
      (%~) SCR SCW = Disproved (\ x -> case x of)
      (%~) SCR SCX = Disproved (\ x -> case x of)
      (%~) SCR SCY = Disproved (\ x -> case x of)
      (%~) SCR SCZ = Disproved (\ x -> case x of)
      (%~) SCS SCA = Disproved (\ x -> case x of)
      (%~) SCS SCB = Disproved (\ x -> case x of)
      (%~) SCS SCC = Disproved (\ x -> case x of)
      (%~) SCS SCD = Disproved (\ x -> case x of)
      (%~) SCS SCE = Disproved (\ x -> case x of)
      (%~) SCS SCF = Disproved (\ x -> case x of)
      (%~) SCS SCG = Disproved (\ x -> case x of)
      (%~) SCS SCH = Disproved (\ x -> case x of)
      (%~) SCS SCI = Disproved (\ x -> case x of)
      (%~) SCS SCJ = Disproved (\ x -> case x of)
      (%~) SCS SCK = Disproved (\ x -> case x of)
      (%~) SCS SCL = Disproved (\ x -> case x of)
      (%~) SCS SCM = Disproved (\ x -> case x of)
      (%~) SCS SCN = Disproved (\ x -> case x of)
      (%~) SCS SCO = Disproved (\ x -> case x of)
      (%~) SCS SCP = Disproved (\ x -> case x of)
      (%~) SCS SCQ = Disproved (\ x -> case x of)
      (%~) SCS SCR = Disproved (\ x -> case x of)
      (%~) SCS SCS = Proved Refl
      (%~) SCS SCT = Disproved (\ x -> case x of)
      (%~) SCS SCU = Disproved (\ x -> case x of)
      (%~) SCS SCV = Disproved (\ x -> case x of)
      (%~) SCS SCW = Disproved (\ x -> case x of)
      (%~) SCS SCX = Disproved (\ x -> case x of)
      (%~) SCS SCY = Disproved (\ x -> case x of)
      (%~) SCS SCZ = Disproved (\ x -> case x of)
      (%~) SCT SCA = Disproved (\ x -> case x of)
      (%~) SCT SCB = Disproved (\ x -> case x of)
      (%~) SCT SCC = Disproved (\ x -> case x of)
      (%~) SCT SCD = Disproved (\ x -> case x of)
      (%~) SCT SCE = Disproved (\ x -> case x of)
      (%~) SCT SCF = Disproved (\ x -> case x of)
      (%~) SCT SCG = Disproved (\ x -> case x of)
      (%~) SCT SCH = Disproved (\ x -> case x of)
      (%~) SCT SCI = Disproved (\ x -> case x of)
      (%~) SCT SCJ = Disproved (\ x -> case x of)
      (%~) SCT SCK = Disproved (\ x -> case x of)
      (%~) SCT SCL = Disproved (\ x -> case x of)
      (%~) SCT SCM = Disproved (\ x -> case x of)
      (%~) SCT SCN = Disproved (\ x -> case x of)
      (%~) SCT SCO = Disproved (\ x -> case x of)
      (%~) SCT SCP = Disproved (\ x -> case x of)
      (%~) SCT SCQ = Disproved (\ x -> case x of)
      (%~) SCT SCR = Disproved (\ x -> case x of)
      (%~) SCT SCS = Disproved (\ x -> case x of)
      (%~) SCT SCT = Proved Refl
      (%~) SCT SCU = Disproved (\ x -> case x of)
      (%~) SCT SCV = Disproved (\ x -> case x of)
      (%~) SCT SCW = Disproved (\ x -> case x of)
      (%~) SCT SCX = Disproved (\ x -> case x of)
      (%~) SCT SCY = Disproved (\ x -> case x of)
      (%~) SCT SCZ = Disproved (\ x -> case x of)
      (%~) SCU SCA = Disproved (\ x -> case x of)
      (%~) SCU SCB = Disproved (\ x -> case x of)
      (%~) SCU SCC = Disproved (\ x -> case x of)
      (%~) SCU SCD = Disproved (\ x -> case x of)
      (%~) SCU SCE = Disproved (\ x -> case x of)
      (%~) SCU SCF = Disproved (\ x -> case x of)
      (%~) SCU SCG = Disproved (\ x -> case x of)
      (%~) SCU SCH = Disproved (\ x -> case x of)
      (%~) SCU SCI = Disproved (\ x -> case x of)
      (%~) SCU SCJ = Disproved (\ x -> case x of)
      (%~) SCU SCK = Disproved (\ x -> case x of)
      (%~) SCU SCL = Disproved (\ x -> case x of)
      (%~) SCU SCM = Disproved (\ x -> case x of)
      (%~) SCU SCN = Disproved (\ x -> case x of)
      (%~) SCU SCO = Disproved (\ x -> case x of)
      (%~) SCU SCP = Disproved (\ x -> case x of)
      (%~) SCU SCQ = Disproved (\ x -> case x of)
      (%~) SCU SCR = Disproved (\ x -> case x of)
      (%~) SCU SCS = Disproved (\ x -> case x of)
      (%~) SCU SCT = Disproved (\ x -> case x of)
      (%~) SCU SCU = Proved Refl
      (%~) SCU SCV = Disproved (\ x -> case x of)
      (%~) SCU SCW = Disproved (\ x -> case x of)
      (%~) SCU SCX = Disproved (\ x -> case x of)
      (%~) SCU SCY = Disproved (\ x -> case x of)
      (%~) SCU SCZ = Disproved (\ x -> case x of)
      (%~) SCV SCA = Disproved (\ x -> case x of)
      (%~) SCV SCB = Disproved (\ x -> case x of)
      (%~) SCV SCC = Disproved (\ x -> case x of)
      (%~) SCV SCD = Disproved (\ x -> case x of)
      (%~) SCV SCE = Disproved (\ x -> case x of)
      (%~) SCV SCF = Disproved (\ x -> case x of)
      (%~) SCV SCG = Disproved (\ x -> case x of)
      (%~) SCV SCH = Disproved (\ x -> case x of)
      (%~) SCV SCI = Disproved (\ x -> case x of)
      (%~) SCV SCJ = Disproved (\ x -> case x of)
      (%~) SCV SCK = Disproved (\ x -> case x of)
      (%~) SCV SCL = Disproved (\ x -> case x of)
      (%~) SCV SCM = Disproved (\ x -> case x of)
      (%~) SCV SCN = Disproved (\ x -> case x of)
      (%~) SCV SCO = Disproved (\ x -> case x of)
      (%~) SCV SCP = Disproved (\ x -> case x of)
      (%~) SCV SCQ = Disproved (\ x -> case x of)
      (%~) SCV SCR = Disproved (\ x -> case x of)
      (%~) SCV SCS = Disproved (\ x -> case x of)
      (%~) SCV SCT = Disproved (\ x -> case x of)
      (%~) SCV SCU = Disproved (\ x -> case x of)
      (%~) SCV SCV = Proved Refl
      (%~) SCV SCW = Disproved (\ x -> case x of)
      (%~) SCV SCX = Disproved (\ x -> case x of)
      (%~) SCV SCY = Disproved (\ x -> case x of)
      (%~) SCV SCZ = Disproved (\ x -> case x of)
      (%~) SCW SCA = Disproved (\ x -> case x of)
      (%~) SCW SCB = Disproved (\ x -> case x of)
      (%~) SCW SCC = Disproved (\ x -> case x of)
      (%~) SCW SCD = Disproved (\ x -> case x of)
      (%~) SCW SCE = Disproved (\ x -> case x of)
      (%~) SCW SCF = Disproved (\ x -> case x of)
      (%~) SCW SCG = Disproved (\ x -> case x of)
      (%~) SCW SCH = Disproved (\ x -> case x of)
      (%~) SCW SCI = Disproved (\ x -> case x of)
      (%~) SCW SCJ = Disproved (\ x -> case x of)
      (%~) SCW SCK = Disproved (\ x -> case x of)
      (%~) SCW SCL = Disproved (\ x -> case x of)
      (%~) SCW SCM = Disproved (\ x -> case x of)
      (%~) SCW SCN = Disproved (\ x -> case x of)
      (%~) SCW SCO = Disproved (\ x -> case x of)
      (%~) SCW SCP = Disproved (\ x -> case x of)
      (%~) SCW SCQ = Disproved (\ x -> case x of)
      (%~) SCW SCR = Disproved (\ x -> case x of)
      (%~) SCW SCS = Disproved (\ x -> case x of)
      (%~) SCW SCT = Disproved (\ x -> case x of)
      (%~) SCW SCU = Disproved (\ x -> case x of)
      (%~) SCW SCV = Disproved (\ x -> case x of)
      (%~) SCW SCW = Proved Refl
      (%~) SCW SCX = Disproved (\ x -> case x of)
      (%~) SCW SCY = Disproved (\ x -> case x of)
      (%~) SCW SCZ = Disproved (\ x -> case x of)
      (%~) SCX SCA = Disproved (\ x -> case x of)
      (%~) SCX SCB = Disproved (\ x -> case x of)
      (%~) SCX SCC = Disproved (\ x -> case x of)
      (%~) SCX SCD = Disproved (\ x -> case x of)
      (%~) SCX SCE = Disproved (\ x -> case x of)
      (%~) SCX SCF = Disproved (\ x -> case x of)
      (%~) SCX SCG = Disproved (\ x -> case x of)
      (%~) SCX SCH = Disproved (\ x -> case x of)
      (%~) SCX SCI = Disproved (\ x -> case x of)
      (%~) SCX SCJ = Disproved (\ x -> case x of)
      (%~) SCX SCK = Disproved (\ x -> case x of)
      (%~) SCX SCL = Disproved (\ x -> case x of)
      (%~) SCX SCM = Disproved (\ x -> case x of)
      (%~) SCX SCN = Disproved (\ x -> case x of)
      (%~) SCX SCO = Disproved (\ x -> case x of)
      (%~) SCX SCP = Disproved (\ x -> case x of)
      (%~) SCX SCQ = Disproved (\ x -> case x of)
      (%~) SCX SCR = Disproved (\ x -> case x of)
      (%~) SCX SCS = Disproved (\ x -> case x of)
      (%~) SCX SCT = Disproved (\ x -> case x of)
      (%~) SCX SCU = Disproved (\ x -> case x of)
      (%~) SCX SCV = Disproved (\ x -> case x of)
      (%~) SCX SCW = Disproved (\ x -> case x of)
      (%~) SCX SCX = Proved Refl
      (%~) SCX SCY = Disproved (\ x -> case x of)
      (%~) SCX SCZ = Disproved (\ x -> case x of)
      (%~) SCY SCA = Disproved (\ x -> case x of)
      (%~) SCY SCB = Disproved (\ x -> case x of)
      (%~) SCY SCC = Disproved (\ x -> case x of)
      (%~) SCY SCD = Disproved (\ x -> case x of)
      (%~) SCY SCE = Disproved (\ x -> case x of)
      (%~) SCY SCF = Disproved (\ x -> case x of)
      (%~) SCY SCG = Disproved (\ x -> case x of)
      (%~) SCY SCH = Disproved (\ x -> case x of)
      (%~) SCY SCI = Disproved (\ x -> case x of)
      (%~) SCY SCJ = Disproved (\ x -> case x of)
      (%~) SCY SCK = Disproved (\ x -> case x of)
      (%~) SCY SCL = Disproved (\ x -> case x of)
      (%~) SCY SCM = Disproved (\ x -> case x of)
      (%~) SCY SCN = Disproved (\ x -> case x of)
      (%~) SCY SCO = Disproved (\ x -> case x of)
      (%~) SCY SCP = Disproved (\ x -> case x of)
      (%~) SCY SCQ = Disproved (\ x -> case x of)
      (%~) SCY SCR = Disproved (\ x -> case x of)
      (%~) SCY SCS = Disproved (\ x -> case x of)
      (%~) SCY SCT = Disproved (\ x -> case x of)
      (%~) SCY SCU = Disproved (\ x -> case x of)
      (%~) SCY SCV = Disproved (\ x -> case x of)
      (%~) SCY SCW = Disproved (\ x -> case x of)
      (%~) SCY SCX = Disproved (\ x -> case x of)
      (%~) SCY SCY = Proved Refl
      (%~) SCY SCZ = Disproved (\ x -> case x of)
      (%~) SCZ SCA = Disproved (\ x -> case x of)
      (%~) SCZ SCB = Disproved (\ x -> case x of)
      (%~) SCZ SCC = Disproved (\ x -> case x of)
      (%~) SCZ SCD = Disproved (\ x -> case x of)
      (%~) SCZ SCE = Disproved (\ x -> case x of)
      (%~) SCZ SCF = Disproved (\ x -> case x of)
      (%~) SCZ SCG = Disproved (\ x -> case x of)
      (%~) SCZ SCH = Disproved (\ x -> case x of)
      (%~) SCZ SCI = Disproved (\ x -> case x of)
      (%~) SCZ SCJ = Disproved (\ x -> case x of)
      (%~) SCZ SCK = Disproved (\ x -> case x of)
      (%~) SCZ SCL = Disproved (\ x -> case x of)
      (%~) SCZ SCM = Disproved (\ x -> case x of)
      (%~) SCZ SCN = Disproved (\ x -> case x of)
      (%~) SCZ SCO = Disproved (\ x -> case x of)
      (%~) SCZ SCP = Disproved (\ x -> case x of)
      (%~) SCZ SCQ = Disproved (\ x -> case x of)
      (%~) SCZ SCR = Disproved (\ x -> case x of)
      (%~) SCZ SCS = Disproved (\ x -> case x of)
      (%~) SCZ SCT = Disproved (\ x -> case x of)
      (%~) SCZ SCU = Disproved (\ x -> case x of)
      (%~) SCZ SCV = Disproved (\ x -> case x of)
      (%~) SCZ SCW = Disproved (\ x -> case x of)
      (%~) SCZ SCX = Disproved (\ x -> case x of)
      (%~) SCZ SCY = Disproved (\ x -> case x of)
      (%~) SCZ SCZ = Proved Refl
    deriving instance (Data.Singletons.ShowSing.ShowSing U,
                       Data.Singletons.ShowSing.ShowSing Nat) =>
                      Show (Sing (z :: U))
    deriving instance Show (Sing (z :: AChar))
    instance SingI BOOL where
      sing = SBOOL
    instance SingI STRING where
      sing = SSTRING
    instance SingI NAT where
      sing = SNAT
    instance (SingI n, SingI n) =>
             SingI (VEC (n :: U) (n :: Nat)) where
      sing = (SVEC sing) sing
    instance SingI (VECSym0 :: (~>) U ((~>) Nat U)) where
      sing = (singFun2 @VECSym0) SVEC
    instance SingI (TyCon2 VEC :: (~>) U ((~>) Nat U)) where
      sing = (singFun2 @(TyCon2 VEC)) SVEC
    instance SingI d => SingI (VECSym1 (d :: U) :: (~>) Nat U) where
      sing = (singFun1 @(VECSym1 (d :: U))) (SVEC (sing @d))
    instance SingI d =>
             SingI (TyCon1 (VEC (d :: U)) :: (~>) Nat U) where
      sing = (singFun1 @(TyCon1 (VEC (d :: U)))) (SVEC (sing @d))
    instance SingI CA where
      sing = SCA
    instance SingI CB where
      sing = SCB
    instance SingI CC where
      sing = SCC
    instance SingI CD where
      sing = SCD
    instance SingI CE where
      sing = SCE
    instance SingI CF where
      sing = SCF
    instance SingI CG where
      sing = SCG
    instance SingI CH where
      sing = SCH
    instance SingI CI where
      sing = SCI
    instance SingI CJ where
      sing = SCJ
    instance SingI CK where
      sing = SCK
    instance SingI CL where
      sing = SCL
    instance SingI CM where
      sing = SCM
    instance SingI CN where
      sing = SCN
    instance SingI CO where
      sing = SCO
    instance SingI CP where
      sing = SCP
    instance SingI CQ where
      sing = SCQ
    instance SingI CR where
      sing = SCR
    instance SingI CS where
      sing = SCS
    instance SingI CT where
      sing = SCT
    instance SingI CU where
      sing = SCU
    instance SingI CV where
      sing = SCV
    instance SingI CW where
      sing = SCW
    instance SingI CX where
      sing = SCX
    instance SingI CY where
      sing = SCY
    instance SingI CZ where
      sing = SCZ
    instance (SingI n, SingI n) =>
             SingI (Attr (n :: [AChar]) (n :: U)) where
      sing = (SAttr sing) sing
    instance SingI (AttrSym0 :: (~>) [AChar] ((~>) U Attribute)) where
      sing = (singFun2 @AttrSym0) SAttr
    instance SingI (TyCon2 Attr :: (~>) [AChar] ((~>) U Attribute)) where
      sing = (singFun2 @(TyCon2 Attr)) SAttr
    instance SingI d =>
             SingI (AttrSym1 (d :: [AChar]) :: (~>) U Attribute) where
      sing = (singFun1 @(AttrSym1 (d :: [AChar]))) (SAttr (sing @d))
    instance SingI d =>
             SingI (TyCon1 (Attr (d :: [AChar])) :: (~>) U Attribute) where
      sing = (singFun1 @(TyCon1 (Attr (d :: [AChar])))) (SAttr (sing @d))
    instance SingI n => SingI (Sch (n :: [Attribute])) where
      sing = SSch sing
    instance SingI (SchSym0 :: (~>) [Attribute] Schema) where
      sing = (singFun1 @SchSym0) SSch
    instance SingI (TyCon1 Sch :: (~>) [Attribute] Schema) where
      sing = (singFun1 @(TyCon1 Sch)) SSch
GradingClient/Database.hs:0:0:: Splicing declarations
    return [] ======>
GradingClient/Database.hs:(0,0)-(0,0): Splicing expression
    cases ''Row [| r |] [| changeId (n ++ (getId r)) r |]
  ======>
    case r of
      EmptyRow _ -> (changeId (((++) n) (getId r))) r
      ConsRow _ _ -> (changeId (((++) n) (getId r))) r