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