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