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