GradingClient/Database.hs:0:0: Splicing declarations
    singletons
      [d| data Nat
            = Zero | Succ Nat
            deriving (Eq, Ord) |]
  ======>
    GradingClient/Database.hs:(0,0)-(0,0)
    data Nat
      = Zero | Succ Nat
      deriving (Eq, Ord)
    type family Equals_0123456789 (a :: Nat) (b :: Nat) :: Bool where
      Equals_0123456789 Zero Zero = True
      Equals_0123456789 (Succ a) (Succ b) = (==) a b
      Equals_0123456789 (a :: Nat) (b :: Nat) = False
    type instance (==) (a :: Nat) (b :: Nat) = Equals_0123456789 a b
    data instance Sing (z :: Nat)
      = z ~ Zero => SZero |
        forall (n :: Nat). z ~ Succ n => SSucc (Sing n)
    type SNat (z :: Nat) = Sing z
    instance SingKind (KProxy :: KProxy Nat) where
      type DemoteRep (KProxy :: KProxy Nat) = Nat
      fromSing SZero = Zero
      fromSing (SSucc b) = Succ (fromSing b)
      toSing Zero = SomeSing SZero
      toSing (Succ b)
        = case toSing b :: SomeSing (KProxy :: KProxy Nat) of {
            SomeSing c -> SomeSing (SSucc c) }
    instance SEq (KProxy :: KProxy Nat) where
      (%:==) SZero SZero = STrue
      (%:==) SZero (SSucc _) = SFalse
      (%:==) (SSucc _) SZero = SFalse
      (%:==) (SSucc a) (SSucc b) = (%:==) a b
    instance SDecide (KProxy :: KProxy Nat) where
      (%~) SZero SZero = Proved Refl
      (%~) SZero (SSucc _)
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) (SSucc _) SZero
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) (SSucc a) (SSucc b)
        = case (%~) a b of {
            Proved Refl -> Proved Refl
            Disproved contra -> Disproved (\ Refl -> contra Refl) }
    instance SingI Zero where
      sing = SZero
    instance SingI n => SingI (Succ (n :: Nat)) where
      sing = SSucc sing
GradingClient/Database.hs: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] |]
  ======>
    GradingClient/Database.hs:(0,0)-(0,0)
    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 GHC.Types.[]) = True
    attrNotIn (Attr name u) (Sch ((Attr name' _) GHC.Types.: t))
      = ((name /= name') && (attrNotIn (Attr name u) (Sch t)))
    disjoint :: Schema -> Schema -> Bool
    disjoint (Sch GHC.Types.[]) _ = True
    disjoint (Sch (h GHC.Types.: t)) s
      = ((attrNotIn h s) && (disjoint (Sch t) s))
    occurs :: [AChar] -> Schema -> Bool
    occurs _ (Sch GHC.Types.[]) = False
    occurs name (Sch ((Attr name' _) GHC.Types.: attrs))
      = ((name == name') || (occurs name (Sch attrs)))
    lookup :: [AChar] -> Schema -> U
    lookup _ (Sch GHC.Types.[]) = undefined
    lookup name (Sch ((Attr name' u) GHC.Types.: attrs))
      = if (name == name') then u else lookup name (Sch attrs)
    type family Equals_0123456789 (a :: U) (b :: U) :: Bool where
      Equals_0123456789 BOOL BOOL = True
      Equals_0123456789 STRING STRING = True
      Equals_0123456789 NAT NAT = True
      Equals_0123456789 (VEC a a) (VEC b b) = (:&&) ((==) a b) ((==) a b)
      Equals_0123456789 (a :: U) (b :: U) = False
    type instance (==) (a :: U) (b :: U) = Equals_0123456789 a b
    type family Equals_0123456789 (a :: AChar)
                                  (b :: AChar) :: Bool where
      Equals_0123456789 CA CA = True
      Equals_0123456789 CB CB = True
      Equals_0123456789 CC CC = True
      Equals_0123456789 CD CD = True
      Equals_0123456789 CE CE = True
      Equals_0123456789 CF CF = True
      Equals_0123456789 CG CG = True
      Equals_0123456789 CH CH = True
      Equals_0123456789 CI CI = True
      Equals_0123456789 CJ CJ = True
      Equals_0123456789 CK CK = True
      Equals_0123456789 CL CL = True
      Equals_0123456789 CM CM = True
      Equals_0123456789 CN CN = True
      Equals_0123456789 CO CO = True
      Equals_0123456789 CP CP = True
      Equals_0123456789 CQ CQ = True
      Equals_0123456789 CR CR = True
      Equals_0123456789 CS CS = True
      Equals_0123456789 CT CT = True
      Equals_0123456789 CU CU = True
      Equals_0123456789 CV CV = True
      Equals_0123456789 CW CW = True
      Equals_0123456789 CX CX = True
      Equals_0123456789 CY CY = True
      Equals_0123456789 CZ CZ = True
      Equals_0123456789 (a :: AChar) (b :: AChar) = False
    type instance (==) (a :: AChar) (b :: AChar) = Equals_0123456789 a b
    type family Append (a :: Schema) (a :: Schema) :: Schema where
      Append (Sch s1) (Sch s2) = Sch ((:++) s1 s2)
    type family AttrNotIn (a :: Attribute) (a :: Schema) :: Bool where
      AttrNotIn z (Sch GHC.Types.[]) = True
      AttrNotIn (Attr name u) (Sch ((GHC.Types.:) (Attr name' z) t)) = (:&&) ((:/=) name name') (AttrNotIn (Attr name u) (Sch t))
    type family Disjoint (a :: Schema) (a :: Schema) :: Bool where
      Disjoint (Sch GHC.Types.[]) z = True
      Disjoint (Sch ((GHC.Types.:) h t)) s = (:&&) (AttrNotIn h s) (Disjoint (Sch t) s)
    type family Occurs (a :: [AChar]) (a :: Schema) :: Bool where
      Occurs z (Sch GHC.Types.[]) = False
      Occurs name (Sch ((GHC.Types.:) (Attr name' z) attrs)) = (:||) ((:==) name name') (Occurs name (Sch attrs))
    type family Lookup (a :: [AChar]) (a :: Schema) :: U where
      Lookup z (Sch GHC.Types.[]) = Any
      Lookup name (Sch ((GHC.Types.:) (Attr name' u) attrs)) = If ((:==) name name') u (Lookup name (Sch attrs))
    data instance Sing (z :: U)
      = z ~ BOOL => SBOOL |
        z ~ STRING => SSTRING |
        z ~ NAT => SNAT |
        forall (n :: U) (n :: Nat). z ~ VEC n n => SVEC (Sing n) (Sing n)
    type SU (z :: U) = Sing z
    instance SingKind (KProxy :: KProxy U) where
      type DemoteRep (KProxy :: KProxy 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 b)
        = case
              (toSing b :: SomeSing (KProxy :: KProxy U), 
               toSing b :: SomeSing (KProxy :: KProxy Nat))
          of {
            (SomeSing c, SomeSing c) -> SomeSing (SVEC c c) }
    instance SEq (KProxy :: KProxy 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 (KProxy :: KProxy U) where
      (%~) SBOOL SBOOL = Proved Refl
      (%~) SBOOL SSTRING
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SBOOL SNAT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SBOOL (SVEC _ _)
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SSTRING SBOOL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SSTRING SSTRING = Proved Refl
      (%~) SSTRING SNAT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SSTRING (SVEC _ _)
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SNAT SBOOL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SNAT SSTRING
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SNAT SNAT = Proved Refl
      (%~) SNAT (SVEC _ _)
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) (SVEC _ _) SBOOL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) (SVEC _ _) SSTRING
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) (SVEC _ _) SNAT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) (SVEC a a) (SVEC b b)
        = case ((%~) a b, (%~) a b) of {
            (Proved Refl, Proved Refl) -> Proved Refl
            (Disproved contra, _) -> Disproved (\ Refl -> contra Refl)
            (_, Disproved contra) -> Disproved (\ Refl -> contra Refl) }
    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
    data instance Sing (z :: AChar)
      = z ~ CA => SCA |
        z ~ CB => SCB |
        z ~ CC => SCC |
        z ~ CD => SCD |
        z ~ CE => SCE |
        z ~ CF => SCF |
        z ~ CG => SCG |
        z ~ CH => SCH |
        z ~ CI => SCI |
        z ~ CJ => SCJ |
        z ~ CK => SCK |
        z ~ CL => SCL |
        z ~ CM => SCM |
        z ~ CN => SCN |
        z ~ CO => SCO |
        z ~ CP => SCP |
        z ~ CQ => SCQ |
        z ~ CR => SCR |
        z ~ CS => SCS |
        z ~ CT => SCT |
        z ~ CU => SCU |
        z ~ CV => SCV |
        z ~ CW => SCW |
        z ~ CX => SCX |
        z ~ CY => SCY |
        z ~ CZ => SCZ
    type SAChar (z :: AChar) = Sing z
    instance SingKind (KProxy :: KProxy AChar) where
      type DemoteRep (KProxy :: KProxy 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
    instance SEq (KProxy :: KProxy 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 (KProxy :: KProxy AChar) where
      (%~) SCA SCA = Proved Refl
      (%~) SCA SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCA SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCB = Proved Refl
      (%~) SCB SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCB SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCC = Proved Refl
      (%~) SCC SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCC SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCD = Proved Refl
      (%~) SCD SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCD SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCE = Proved Refl
      (%~) SCE SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCE SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCF = Proved Refl
      (%~) SCF SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCF SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCG = Proved Refl
      (%~) SCG SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCG SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCH = Proved Refl
      (%~) SCH SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCH SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCI = Proved Refl
      (%~) SCI SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCI SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCJ = Proved Refl
      (%~) SCJ SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCJ SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCK = Proved Refl
      (%~) SCK SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCK SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCL = Proved Refl
      (%~) SCL SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCL SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCM = Proved Refl
      (%~) SCM SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCM SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCN = Proved Refl
      (%~) SCN SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCN SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCO = Proved Refl
      (%~) SCO SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCO SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCP = Proved Refl
      (%~) SCP SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCP SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCQ = Proved Refl
      (%~) SCQ SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCQ SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCR = Proved Refl
      (%~) SCR SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCR SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCS = Proved Refl
      (%~) SCS SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCS SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCT = Proved Refl
      (%~) SCT SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCT SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCU = Proved Refl
      (%~) SCU SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCU SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCV = Proved Refl
      (%~) SCV SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCV SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCW = Proved Refl
      (%~) SCW SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCW SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCX = Proved Refl
      (%~) SCX SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCX SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCY SCY = Proved Refl
      (%~) SCY SCZ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCA
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCB
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCC
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCD
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCE
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCF
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCG
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCH
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCI
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCJ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCK
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCL
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCM
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCN
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCO
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCP
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCQ
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCR
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCS
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCT
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCU
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCV
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCW
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCX
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCY
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      (%~) SCZ SCZ = Proved Refl
    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
    data instance Sing (z :: Attribute)
      = forall (n :: [AChar]) (n :: U). z ~ Attr n n =>
        SAttr (Sing n) (Sing n)
    type SAttribute (z :: Attribute) = Sing z
    instance SingKind (KProxy :: KProxy Attribute) where
      type DemoteRep (KProxy :: KProxy Attribute) = Attribute
      fromSing (SAttr b b) = Attr (fromSing b) (fromSing b)
      toSing (Attr b b)
        = case
              (toSing b :: SomeSing (KProxy :: KProxy [AChar]), 
               toSing b :: SomeSing (KProxy :: KProxy U))
          of {
            (SomeSing c, SomeSing c) -> SomeSing (SAttr c c) }
    instance (SingI n, SingI n) =>
             SingI (Attr (n :: [AChar]) (n :: U)) where
      sing = SAttr sing sing
    data instance Sing (z :: Schema)
      = forall (n :: [Attribute]). z ~ Sch n => SSch (Sing n)
    type SSchema (z :: Schema) = Sing z
    instance SingKind (KProxy :: KProxy Schema) where
      type DemoteRep (KProxy :: KProxy Schema) = Schema
      fromSing (SSch b) = Sch (fromSing b)
      toSing (Sch b)
        = case toSing b :: SomeSing (KProxy :: KProxy [Attribute]) of {
            SomeSing c -> SomeSing (SSch c) }
    instance SingI n => SingI (Sch (n :: [Attribute])) where
      sing = SSch sing
    sAppend ::
      forall (t :: Schema) (t :: Schema).
      Sing t -> Sing t -> Sing (Append t t)
    sAppend (SSch s1) (SSch s2) = SSch ((%:++) s1 s2)
    sAttrNotIn ::
      forall (t :: Attribute) (t :: Schema).
      Sing t -> Sing t -> Sing (AttrNotIn t t)
    sAttrNotIn _ (SSch SNil) = STrue
    sAttrNotIn (SAttr name u) (SSch (SCons (SAttr name' _) t))
      = (%:&&) ((%:/=) name name') (sAttrNotIn (SAttr name u) (SSch t))
    sDisjoint ::
      forall (t :: Schema) (t :: Schema).
      Sing t -> Sing t -> Sing (Disjoint t t)
    sDisjoint (SSch SNil) _ = STrue
    sDisjoint (SSch (SCons h t)) s
      = (%:&&) (sAttrNotIn h s) (sDisjoint (SSch t) s)
    sOccurs ::
      forall (t :: [AChar]) (t :: Schema).
      Sing t -> Sing t -> Sing (Occurs t t)
    sOccurs _ (SSch SNil) = SFalse
    sOccurs name (SSch (SCons (SAttr name' _) attrs))
      = (%:||) ((%:==) name name') (sOccurs name (SSch attrs))
    sLookup ::
      forall (t :: [AChar]) (t :: Schema).
      Sing t -> Sing t -> Sing (Lookup t t)
    sLookup _ (SSch SNil) = undefined
    sLookup name (SSch (SCons (SAttr name' u) attrs))
      = sIf ((%:==) name name') u (sLookup name (SSch attrs))
GradingClient/Database.hs:0:0: Splicing declarations
    return [] ======> GradingClient/Database.hs:0:0:
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 }