GradingClient/Database.hs:0:0: Splicing declarations singletons [d| data Nat = Zero | Succ Nat deriving (Eq, Ord) |] ======> GradingClient/Database.hs:(0,0)-(0,0) data Nat = Zero | Succ Nat deriving (Eq, Ord) type instance (:==) Zero Zero = TrueSym0 type instance (:==) Zero (Succ b) = FalseSym0 type instance (:==) (Succ a) Zero = FalseSym0 type instance (:==) (Succ a) (Succ b) = :== a b type NatTyCtor = Nat type NatTyCtorSym0 = NatTyCtor type ZeroSym0 = Zero data SuccSym0 (k :: TyFun Nat Nat) type instance Apply SuccSym0 a = Succ a data instance Sing (z :: Nat) = z ~ Zero => SZero | forall (n :: Nat). z ~ Succ n => SSucc (Sing n) type SNat (z :: Nat) = Sing z instance SingKind (KProxy :: KProxy Nat) where type instance DemoteRep (KProxy :: KProxy Nat) = Nat fromSing SZero = Zero fromSing (SSucc b) = Succ (fromSing b) toSing Zero = SomeSing SZero toSing (Succ b) = case toSing b :: SomeSing (KProxy :: KProxy Nat) of { SomeSing c -> SomeSing (SSucc c) } instance SEq (KProxy :: KProxy Nat) where %:== SZero SZero = STrue %:== SZero (SSucc _) = SFalse %:== (SSucc _) SZero = SFalse %:== (SSucc a) (SSucc b) = (%:==) a b instance SDecide (KProxy :: KProxy Nat) where %~ SZero SZero = Proved Refl %~ SZero (SSucc _) = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ (SSucc _) SZero = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ (SSucc a) (SSucc b) = case (%~) a b of { Proved Refl -> Proved Refl Disproved contra -> Disproved (\ Refl -> contra Refl) } instance SingI Zero where sing = SZero instance SingI n => SingI (Succ (n :: Nat)) where sing = SSucc sing GradingClient/Database.hs:0:0: Splicing declarations singletons [d| append :: Schema -> Schema -> Schema append (Sch s1) (Sch s2) = Sch (s1 ++ s2) attrNotIn :: Attribute -> Schema -> Bool attrNotIn _ (Sch []) = True attrNotIn (Attr name u) (Sch ((Attr name' _) : t)) = (name /= name') && (attrNotIn (Attr name u) (Sch t)) disjoint :: Schema -> Schema -> Bool disjoint (Sch []) _ = True disjoint (Sch (h : t)) s = (attrNotIn h s) && (disjoint (Sch t) s) occurs :: [AChar] -> Schema -> Bool occurs _ (Sch []) = False occurs name (Sch ((Attr name' _) : attrs)) = name == name' || occurs name (Sch attrs) lookup :: [AChar] -> Schema -> U lookup _ (Sch []) = undefined lookup name (Sch ((Attr name' u) : attrs)) = if name == name' then u else lookup name (Sch attrs) data U = BOOL | STRING | NAT | VEC U Nat deriving (Read, Eq, Show) data AChar = CA | CB | CC | CD | CE | CF | CG | CH | CI | CJ | CK | CL | CM | CN | CO | CP | CQ | CR | CS | CT | CU | CV | CW | CX | CY | CZ deriving (Read, Show, Eq) data Attribute = Attr [AChar] U data Schema = Sch [Attribute] |] ======> GradingClient/Database.hs:(0,0)-(0,0) data U = BOOL | STRING | NAT | VEC U Nat deriving (Read, Eq, Show) data AChar = CA | CB | CC | CD | CE | CF | CG | CH | CI | CJ | CK | CL | CM | CN | CO | CP | CQ | CR | CS | CT | CU | CV | CW | CX | CY | CZ deriving (Read, Show, Eq) data Attribute = Attr [AChar] U data Schema = Sch [Attribute] append :: Schema -> Schema -> Schema append (Sch s1) (Sch s2) = Sch (s1 ++ s2) attrNotIn :: Attribute -> Schema -> Bool attrNotIn _ (Sch GHC.Types.[]) = True attrNotIn (Attr name u) (Sch ((Attr name' _) GHC.Types.: t)) = ((name /= name') && (attrNotIn (Attr name u) (Sch t))) disjoint :: Schema -> Schema -> Bool disjoint (Sch GHC.Types.[]) _ = True disjoint (Sch (h GHC.Types.: t)) s = ((attrNotIn h s) && (disjoint (Sch t) s)) occurs :: [AChar] -> Schema -> Bool occurs _ (Sch GHC.Types.[]) = False occurs name (Sch ((Attr name' _) GHC.Types.: attrs)) = ((name == name') || (occurs name (Sch attrs))) lookup :: [AChar] -> Schema -> U lookup _ (Sch GHC.Types.[]) = undefined lookup name (Sch ((Attr name' u) GHC.Types.: attrs)) = if (name == name') then u else lookup name (Sch attrs) type instance (:==) BOOL BOOL = TrueSym0 type instance (:==) BOOL STRING = FalseSym0 type instance (:==) BOOL NAT = FalseSym0 type instance (:==) BOOL (VEC b b) = FalseSym0 type instance (:==) STRING BOOL = FalseSym0 type instance (:==) STRING STRING = TrueSym0 type instance (:==) STRING NAT = FalseSym0 type instance (:==) STRING (VEC b b) = FalseSym0 type instance (:==) NAT BOOL = FalseSym0 type instance (:==) NAT STRING = FalseSym0 type instance (:==) NAT NAT = TrueSym0 type instance (:==) NAT (VEC b b) = FalseSym0 type instance (:==) (VEC a a) BOOL = FalseSym0 type instance (:==) (VEC a a) STRING = FalseSym0 type instance (:==) (VEC a a) NAT = FalseSym0 type instance (:==) (VEC a a) (VEC b b) = :&& (:== a b) (:== a b) type UTyCtor = U type UTyCtorSym0 = UTyCtor type BOOLSym0 = BOOL type STRINGSym0 = STRING type NATSym0 = NAT data VECSym1 (l :: U) (l :: TyFun Nat U) data VECSym0 (k :: TyFun U (TyFun Nat U -> *)) type instance Apply (VECSym1 a) a = VEC a a type instance Apply VECSym0 a = VECSym1 a type instance (:==) CA CA = TrueSym0 type instance (:==) CA CB = FalseSym0 type instance (:==) CA CC = FalseSym0 type instance (:==) CA CD = FalseSym0 type instance (:==) CA CE = FalseSym0 type instance (:==) CA CF = FalseSym0 type instance (:==) CA CG = FalseSym0 type instance (:==) CA CH = FalseSym0 type instance (:==) CA CI = FalseSym0 type instance (:==) CA CJ = FalseSym0 type instance (:==) CA CK = FalseSym0 type instance (:==) CA CL = FalseSym0 type instance (:==) CA CM = FalseSym0 type instance (:==) CA CN = FalseSym0 type instance (:==) CA CO = FalseSym0 type instance (:==) CA CP = FalseSym0 type instance (:==) CA CQ = FalseSym0 type instance (:==) CA CR = FalseSym0 type instance (:==) CA CS = FalseSym0 type instance (:==) CA CT = FalseSym0 type instance (:==) CA CU = FalseSym0 type instance (:==) CA CV = FalseSym0 type instance (:==) CA CW = FalseSym0 type instance (:==) CA CX = FalseSym0 type instance (:==) CA CY = FalseSym0 type instance (:==) CA CZ = FalseSym0 type instance (:==) CB CA = FalseSym0 type instance (:==) CB CB = TrueSym0 type instance (:==) CB CC = FalseSym0 type instance (:==) CB CD = FalseSym0 type instance (:==) CB CE = FalseSym0 type instance (:==) CB CF = FalseSym0 type instance (:==) CB CG = FalseSym0 type instance (:==) CB CH = FalseSym0 type instance (:==) CB CI = FalseSym0 type instance (:==) CB CJ = FalseSym0 type instance (:==) CB CK = FalseSym0 type instance (:==) CB CL = FalseSym0 type instance (:==) CB CM = FalseSym0 type instance (:==) CB CN = FalseSym0 type instance (:==) CB CO = FalseSym0 type instance (:==) CB CP = FalseSym0 type instance (:==) CB CQ = FalseSym0 type instance (:==) CB CR = FalseSym0 type instance (:==) CB CS = FalseSym0 type instance (:==) CB CT = FalseSym0 type instance (:==) CB CU = FalseSym0 type instance (:==) CB CV = FalseSym0 type instance (:==) CB CW = FalseSym0 type instance (:==) CB CX = FalseSym0 type instance (:==) CB CY = FalseSym0 type instance (:==) CB CZ = FalseSym0 type instance (:==) CC CA = FalseSym0 type instance (:==) CC CB = FalseSym0 type instance (:==) CC CC = TrueSym0 type instance (:==) CC CD = FalseSym0 type instance (:==) CC CE = FalseSym0 type instance (:==) CC CF = FalseSym0 type instance (:==) CC CG = FalseSym0 type instance (:==) CC CH = FalseSym0 type instance (:==) CC CI = FalseSym0 type instance (:==) CC CJ = FalseSym0 type instance (:==) CC CK = FalseSym0 type instance (:==) CC CL = FalseSym0 type instance (:==) CC CM = FalseSym0 type instance (:==) CC CN = FalseSym0 type instance (:==) CC CO = FalseSym0 type instance (:==) CC CP = FalseSym0 type instance (:==) CC CQ = FalseSym0 type instance (:==) CC CR = FalseSym0 type instance (:==) CC CS = FalseSym0 type instance (:==) CC CT = FalseSym0 type instance (:==) CC CU = FalseSym0 type instance (:==) CC CV = FalseSym0 type instance (:==) CC CW = FalseSym0 type instance (:==) CC CX = FalseSym0 type instance (:==) CC CY = FalseSym0 type instance (:==) CC CZ = FalseSym0 type instance (:==) CD CA = FalseSym0 type instance (:==) CD CB = FalseSym0 type instance (:==) CD CC = FalseSym0 type instance (:==) CD CD = TrueSym0 type instance (:==) CD CE = FalseSym0 type instance (:==) CD CF = FalseSym0 type instance (:==) CD CG = FalseSym0 type instance (:==) CD CH = FalseSym0 type instance (:==) CD CI = FalseSym0 type instance (:==) CD CJ = FalseSym0 type instance (:==) CD CK = FalseSym0 type instance (:==) CD CL = FalseSym0 type instance (:==) CD CM = FalseSym0 type instance (:==) CD CN = FalseSym0 type instance (:==) CD CO = FalseSym0 type instance (:==) CD CP = FalseSym0 type instance (:==) CD CQ = FalseSym0 type instance (:==) CD CR = FalseSym0 type instance (:==) CD CS = FalseSym0 type instance (:==) CD CT = FalseSym0 type instance (:==) CD CU = FalseSym0 type instance (:==) CD CV = FalseSym0 type instance (:==) CD CW = FalseSym0 type instance (:==) CD CX = FalseSym0 type instance (:==) CD CY = FalseSym0 type instance (:==) CD CZ = FalseSym0 type instance (:==) CE CA = FalseSym0 type instance (:==) CE CB = FalseSym0 type instance (:==) CE CC = FalseSym0 type instance (:==) CE CD = FalseSym0 type instance (:==) CE CE = TrueSym0 type instance (:==) CE CF = FalseSym0 type instance (:==) CE CG = FalseSym0 type instance (:==) CE CH = FalseSym0 type instance (:==) CE CI = FalseSym0 type instance (:==) CE CJ = FalseSym0 type instance (:==) CE CK = FalseSym0 type instance (:==) CE CL = FalseSym0 type instance (:==) CE CM = FalseSym0 type instance (:==) CE CN = FalseSym0 type instance (:==) CE CO = FalseSym0 type instance (:==) CE CP = FalseSym0 type instance (:==) CE CQ = FalseSym0 type instance (:==) CE CR = FalseSym0 type instance (:==) CE CS = FalseSym0 type instance (:==) CE CT = FalseSym0 type instance (:==) CE CU = FalseSym0 type instance (:==) CE CV = FalseSym0 type instance (:==) CE CW = FalseSym0 type instance (:==) CE CX = FalseSym0 type instance (:==) CE CY = FalseSym0 type instance (:==) CE CZ = FalseSym0 type instance (:==) CF CA = FalseSym0 type instance (:==) CF CB = FalseSym0 type instance (:==) CF CC = FalseSym0 type instance (:==) CF CD = FalseSym0 type instance (:==) CF CE = FalseSym0 type instance (:==) CF CF = TrueSym0 type instance (:==) CF CG = FalseSym0 type instance (:==) CF CH = FalseSym0 type instance (:==) CF CI = FalseSym0 type instance (:==) CF CJ = FalseSym0 type instance (:==) CF CK = FalseSym0 type instance (:==) CF CL = FalseSym0 type instance (:==) CF CM = FalseSym0 type instance (:==) CF CN = FalseSym0 type instance (:==) CF CO = FalseSym0 type instance (:==) CF CP = FalseSym0 type instance (:==) CF CQ = FalseSym0 type instance (:==) CF CR = FalseSym0 type instance (:==) CF CS = FalseSym0 type instance (:==) CF CT = FalseSym0 type instance (:==) CF CU = FalseSym0 type instance (:==) CF CV = FalseSym0 type instance (:==) CF CW = FalseSym0 type instance (:==) CF CX = FalseSym0 type instance (:==) CF CY = FalseSym0 type instance (:==) CF CZ = FalseSym0 type instance (:==) CG CA = FalseSym0 type instance (:==) CG CB = FalseSym0 type instance (:==) CG CC = FalseSym0 type instance (:==) CG CD = FalseSym0 type instance (:==) CG CE = FalseSym0 type instance (:==) CG CF = FalseSym0 type instance (:==) CG CG = TrueSym0 type instance (:==) CG CH = FalseSym0 type instance (:==) CG CI = FalseSym0 type instance (:==) CG CJ = FalseSym0 type instance (:==) CG CK = FalseSym0 type instance (:==) CG CL = FalseSym0 type instance (:==) CG CM = FalseSym0 type instance (:==) CG CN = FalseSym0 type instance (:==) CG CO = FalseSym0 type instance (:==) CG CP = FalseSym0 type instance (:==) CG CQ = FalseSym0 type instance (:==) CG CR = FalseSym0 type instance (:==) CG CS = FalseSym0 type instance (:==) CG CT = FalseSym0 type instance (:==) CG CU = FalseSym0 type instance (:==) CG CV = FalseSym0 type instance (:==) CG CW = FalseSym0 type instance (:==) CG CX = FalseSym0 type instance (:==) CG CY = FalseSym0 type instance (:==) CG CZ = FalseSym0 type instance (:==) CH CA = FalseSym0 type instance (:==) CH CB = FalseSym0 type instance (:==) CH CC = FalseSym0 type instance (:==) CH CD = FalseSym0 type instance (:==) CH CE = FalseSym0 type instance (:==) CH CF = FalseSym0 type instance (:==) CH CG = FalseSym0 type instance (:==) CH CH = TrueSym0 type instance (:==) CH CI = FalseSym0 type instance (:==) CH CJ = FalseSym0 type instance (:==) CH CK = FalseSym0 type instance (:==) CH CL = FalseSym0 type instance (:==) CH CM = FalseSym0 type instance (:==) CH CN = FalseSym0 type instance (:==) CH CO = FalseSym0 type instance (:==) CH CP = FalseSym0 type instance (:==) CH CQ = FalseSym0 type instance (:==) CH CR = FalseSym0 type instance (:==) CH CS = FalseSym0 type instance (:==) CH CT = FalseSym0 type instance (:==) CH CU = FalseSym0 type instance (:==) CH CV = FalseSym0 type instance (:==) CH CW = FalseSym0 type instance (:==) CH CX = FalseSym0 type instance (:==) CH CY = FalseSym0 type instance (:==) CH CZ = FalseSym0 type instance (:==) CI CA = FalseSym0 type instance (:==) CI CB = FalseSym0 type instance (:==) CI CC = FalseSym0 type instance (:==) CI CD = FalseSym0 type instance (:==) CI CE = FalseSym0 type instance (:==) CI CF = FalseSym0 type instance (:==) CI CG = FalseSym0 type instance (:==) CI CH = FalseSym0 type instance (:==) CI CI = TrueSym0 type instance (:==) CI CJ = FalseSym0 type instance (:==) CI CK = FalseSym0 type instance (:==) CI CL = FalseSym0 type instance (:==) CI CM = FalseSym0 type instance (:==) CI CN = FalseSym0 type instance (:==) CI CO = FalseSym0 type instance (:==) CI CP = FalseSym0 type instance (:==) CI CQ = FalseSym0 type instance (:==) CI CR = FalseSym0 type instance (:==) CI CS = FalseSym0 type instance (:==) CI CT = FalseSym0 type instance (:==) CI CU = FalseSym0 type instance (:==) CI CV = FalseSym0 type instance (:==) CI CW = FalseSym0 type instance (:==) CI CX = FalseSym0 type instance (:==) CI CY = FalseSym0 type instance (:==) CI CZ = FalseSym0 type instance (:==) CJ CA = FalseSym0 type instance (:==) CJ CB = FalseSym0 type instance (:==) CJ CC = FalseSym0 type instance (:==) CJ CD = FalseSym0 type instance (:==) CJ CE = FalseSym0 type instance (:==) CJ CF = FalseSym0 type instance (:==) CJ CG = FalseSym0 type instance (:==) CJ CH = FalseSym0 type instance (:==) CJ CI = FalseSym0 type instance (:==) CJ CJ = TrueSym0 type instance (:==) CJ CK = FalseSym0 type instance (:==) CJ CL = FalseSym0 type instance (:==) CJ CM = FalseSym0 type instance (:==) CJ CN = FalseSym0 type instance (:==) CJ CO = FalseSym0 type instance (:==) CJ CP = FalseSym0 type instance (:==) CJ CQ = FalseSym0 type instance (:==) CJ CR = FalseSym0 type instance (:==) CJ CS = FalseSym0 type instance (:==) CJ CT = FalseSym0 type instance (:==) CJ CU = FalseSym0 type instance (:==) CJ CV = FalseSym0 type instance (:==) CJ CW = FalseSym0 type instance (:==) CJ CX = FalseSym0 type instance (:==) CJ CY = FalseSym0 type instance (:==) CJ CZ = FalseSym0 type instance (:==) CK CA = FalseSym0 type instance (:==) CK CB = FalseSym0 type instance (:==) CK CC = FalseSym0 type instance (:==) CK CD = FalseSym0 type instance (:==) CK CE = FalseSym0 type instance (:==) CK CF = FalseSym0 type instance (:==) CK CG = FalseSym0 type instance (:==) CK CH = FalseSym0 type instance (:==) CK CI = FalseSym0 type instance (:==) CK CJ = FalseSym0 type instance (:==) CK CK = TrueSym0 type instance (:==) CK CL = FalseSym0 type instance (:==) CK CM = FalseSym0 type instance (:==) CK CN = FalseSym0 type instance (:==) CK CO = FalseSym0 type instance (:==) CK CP = FalseSym0 type instance (:==) CK CQ = FalseSym0 type instance (:==) CK CR = FalseSym0 type instance (:==) CK CS = FalseSym0 type instance (:==) CK CT = FalseSym0 type instance (:==) CK CU = FalseSym0 type instance (:==) CK CV = FalseSym0 type instance (:==) CK CW = FalseSym0 type instance (:==) CK CX = FalseSym0 type instance (:==) CK CY = FalseSym0 type instance (:==) CK CZ = FalseSym0 type instance (:==) CL CA = FalseSym0 type instance (:==) CL CB = FalseSym0 type instance (:==) CL CC = FalseSym0 type instance (:==) CL CD = FalseSym0 type instance (:==) CL CE = FalseSym0 type instance (:==) CL CF = FalseSym0 type instance (:==) CL CG = FalseSym0 type instance (:==) CL CH = FalseSym0 type instance (:==) CL CI = FalseSym0 type instance (:==) CL CJ = FalseSym0 type instance (:==) CL CK = FalseSym0 type instance (:==) CL CL = TrueSym0 type instance (:==) CL CM = FalseSym0 type instance (:==) CL CN = FalseSym0 type instance (:==) CL CO = FalseSym0 type instance (:==) CL CP = FalseSym0 type instance (:==) CL CQ = FalseSym0 type instance (:==) CL CR = FalseSym0 type instance (:==) CL CS = FalseSym0 type instance (:==) CL CT = FalseSym0 type instance (:==) CL CU = FalseSym0 type instance (:==) CL CV = FalseSym0 type instance (:==) CL CW = FalseSym0 type instance (:==) CL CX = FalseSym0 type instance (:==) CL CY = FalseSym0 type instance (:==) CL CZ = FalseSym0 type instance (:==) CM CA = FalseSym0 type instance (:==) CM CB = FalseSym0 type instance (:==) CM CC = FalseSym0 type instance (:==) CM CD = FalseSym0 type instance (:==) CM CE = FalseSym0 type instance (:==) CM CF = FalseSym0 type instance (:==) CM CG = FalseSym0 type instance (:==) CM CH = FalseSym0 type instance (:==) CM CI = FalseSym0 type instance (:==) CM CJ = FalseSym0 type instance (:==) CM CK = FalseSym0 type instance (:==) CM CL = FalseSym0 type instance (:==) CM CM = TrueSym0 type instance (:==) CM CN = FalseSym0 type instance (:==) CM CO = FalseSym0 type instance (:==) CM CP = FalseSym0 type instance (:==) CM CQ = FalseSym0 type instance (:==) CM CR = FalseSym0 type instance (:==) CM CS = FalseSym0 type instance (:==) CM CT = FalseSym0 type instance (:==) CM CU = FalseSym0 type instance (:==) CM CV = FalseSym0 type instance (:==) CM CW = FalseSym0 type instance (:==) CM CX = FalseSym0 type instance (:==) CM CY = FalseSym0 type instance (:==) CM CZ = FalseSym0 type instance (:==) CN CA = FalseSym0 type instance (:==) CN CB = FalseSym0 type instance (:==) CN CC = FalseSym0 type instance (:==) CN CD = FalseSym0 type instance (:==) CN CE = FalseSym0 type instance (:==) CN CF = FalseSym0 type instance (:==) CN CG = FalseSym0 type instance (:==) CN CH = FalseSym0 type instance (:==) CN CI = FalseSym0 type instance (:==) CN CJ = FalseSym0 type instance (:==) CN CK = FalseSym0 type instance (:==) CN CL = FalseSym0 type instance (:==) CN CM = FalseSym0 type instance (:==) CN CN = TrueSym0 type instance (:==) CN CO = FalseSym0 type instance (:==) CN CP = FalseSym0 type instance (:==) CN CQ = FalseSym0 type instance (:==) CN CR = FalseSym0 type instance (:==) CN CS = FalseSym0 type instance (:==) CN CT = FalseSym0 type instance (:==) CN CU = FalseSym0 type instance (:==) CN CV = FalseSym0 type instance (:==) CN CW = FalseSym0 type instance (:==) CN CX = FalseSym0 type instance (:==) CN CY = FalseSym0 type instance (:==) CN CZ = FalseSym0 type instance (:==) CO CA = FalseSym0 type instance (:==) CO CB = FalseSym0 type instance (:==) CO CC = FalseSym0 type instance (:==) CO CD = FalseSym0 type instance (:==) CO CE = FalseSym0 type instance (:==) CO CF = FalseSym0 type instance (:==) CO CG = FalseSym0 type instance (:==) CO CH = FalseSym0 type instance (:==) CO CI = FalseSym0 type instance (:==) CO CJ = FalseSym0 type instance (:==) CO CK = FalseSym0 type instance (:==) CO CL = FalseSym0 type instance (:==) CO CM = FalseSym0 type instance (:==) CO CN = FalseSym0 type instance (:==) CO CO = TrueSym0 type instance (:==) CO CP = FalseSym0 type instance (:==) CO CQ = FalseSym0 type instance (:==) CO CR = FalseSym0 type instance (:==) CO CS = FalseSym0 type instance (:==) CO CT = FalseSym0 type instance (:==) CO CU = FalseSym0 type instance (:==) CO CV = FalseSym0 type instance (:==) CO CW = FalseSym0 type instance (:==) CO CX = FalseSym0 type instance (:==) CO CY = FalseSym0 type instance (:==) CO CZ = FalseSym0 type instance (:==) CP CA = FalseSym0 type instance (:==) CP CB = FalseSym0 type instance (:==) CP CC = FalseSym0 type instance (:==) CP CD = FalseSym0 type instance (:==) CP CE = FalseSym0 type instance (:==) CP CF = FalseSym0 type instance (:==) CP CG = FalseSym0 type instance (:==) CP CH = FalseSym0 type instance (:==) CP CI = FalseSym0 type instance (:==) CP CJ = FalseSym0 type instance (:==) CP CK = FalseSym0 type instance (:==) CP CL = FalseSym0 type instance (:==) CP CM = FalseSym0 type instance (:==) CP CN = FalseSym0 type instance (:==) CP CO = FalseSym0 type instance (:==) CP CP = TrueSym0 type instance (:==) CP CQ = FalseSym0 type instance (:==) CP CR = FalseSym0 type instance (:==) CP CS = FalseSym0 type instance (:==) CP CT = FalseSym0 type instance (:==) CP CU = FalseSym0 type instance (:==) CP CV = FalseSym0 type instance (:==) CP CW = FalseSym0 type instance (:==) CP CX = FalseSym0 type instance (:==) CP CY = FalseSym0 type instance (:==) CP CZ = FalseSym0 type instance (:==) CQ CA = FalseSym0 type instance (:==) CQ CB = FalseSym0 type instance (:==) CQ CC = FalseSym0 type instance (:==) CQ CD = FalseSym0 type instance (:==) CQ CE = FalseSym0 type instance (:==) CQ CF = FalseSym0 type instance (:==) CQ CG = FalseSym0 type instance (:==) CQ CH = FalseSym0 type instance (:==) CQ CI = FalseSym0 type instance (:==) CQ CJ = FalseSym0 type instance (:==) CQ CK = FalseSym0 type instance (:==) CQ CL = FalseSym0 type instance (:==) CQ CM = FalseSym0 type instance (:==) CQ CN = FalseSym0 type instance (:==) CQ CO = FalseSym0 type instance (:==) CQ CP = FalseSym0 type instance (:==) CQ CQ = TrueSym0 type instance (:==) CQ CR = FalseSym0 type instance (:==) CQ CS = FalseSym0 type instance (:==) CQ CT = FalseSym0 type instance (:==) CQ CU = FalseSym0 type instance (:==) CQ CV = FalseSym0 type instance (:==) CQ CW = FalseSym0 type instance (:==) CQ CX = FalseSym0 type instance (:==) CQ CY = FalseSym0 type instance (:==) CQ CZ = FalseSym0 type instance (:==) CR CA = FalseSym0 type instance (:==) CR CB = FalseSym0 type instance (:==) CR CC = FalseSym0 type instance (:==) CR CD = FalseSym0 type instance (:==) CR CE = FalseSym0 type instance (:==) CR CF = FalseSym0 type instance (:==) CR CG = FalseSym0 type instance (:==) CR CH = FalseSym0 type instance (:==) CR CI = FalseSym0 type instance (:==) CR CJ = FalseSym0 type instance (:==) CR CK = FalseSym0 type instance (:==) CR CL = FalseSym0 type instance (:==) CR CM = FalseSym0 type instance (:==) CR CN = FalseSym0 type instance (:==) CR CO = FalseSym0 type instance (:==) CR CP = FalseSym0 type instance (:==) CR CQ = FalseSym0 type instance (:==) CR CR = TrueSym0 type instance (:==) CR CS = FalseSym0 type instance (:==) CR CT = FalseSym0 type instance (:==) CR CU = FalseSym0 type instance (:==) CR CV = FalseSym0 type instance (:==) CR CW = FalseSym0 type instance (:==) CR CX = FalseSym0 type instance (:==) CR CY = FalseSym0 type instance (:==) CR CZ = FalseSym0 type instance (:==) CS CA = FalseSym0 type instance (:==) CS CB = FalseSym0 type instance (:==) CS CC = FalseSym0 type instance (:==) CS CD = FalseSym0 type instance (:==) CS CE = FalseSym0 type instance (:==) CS CF = FalseSym0 type instance (:==) CS CG = FalseSym0 type instance (:==) CS CH = FalseSym0 type instance (:==) CS CI = FalseSym0 type instance (:==) CS CJ = FalseSym0 type instance (:==) CS CK = FalseSym0 type instance (:==) CS CL = FalseSym0 type instance (:==) CS CM = FalseSym0 type instance (:==) CS CN = FalseSym0 type instance (:==) CS CO = FalseSym0 type instance (:==) CS CP = FalseSym0 type instance (:==) CS CQ = FalseSym0 type instance (:==) CS CR = FalseSym0 type instance (:==) CS CS = TrueSym0 type instance (:==) CS CT = FalseSym0 type instance (:==) CS CU = FalseSym0 type instance (:==) CS CV = FalseSym0 type instance (:==) CS CW = FalseSym0 type instance (:==) CS CX = FalseSym0 type instance (:==) CS CY = FalseSym0 type instance (:==) CS CZ = FalseSym0 type instance (:==) CT CA = FalseSym0 type instance (:==) CT CB = FalseSym0 type instance (:==) CT CC = FalseSym0 type instance (:==) CT CD = FalseSym0 type instance (:==) CT CE = FalseSym0 type instance (:==) CT CF = FalseSym0 type instance (:==) CT CG = FalseSym0 type instance (:==) CT CH = FalseSym0 type instance (:==) CT CI = FalseSym0 type instance (:==) CT CJ = FalseSym0 type instance (:==) CT CK = FalseSym0 type instance (:==) CT CL = FalseSym0 type instance (:==) CT CM = FalseSym0 type instance (:==) CT CN = FalseSym0 type instance (:==) CT CO = FalseSym0 type instance (:==) CT CP = FalseSym0 type instance (:==) CT CQ = FalseSym0 type instance (:==) CT CR = FalseSym0 type instance (:==) CT CS = FalseSym0 type instance (:==) CT CT = TrueSym0 type instance (:==) CT CU = FalseSym0 type instance (:==) CT CV = FalseSym0 type instance (:==) CT CW = FalseSym0 type instance (:==) CT CX = FalseSym0 type instance (:==) CT CY = FalseSym0 type instance (:==) CT CZ = FalseSym0 type instance (:==) CU CA = FalseSym0 type instance (:==) CU CB = FalseSym0 type instance (:==) CU CC = FalseSym0 type instance (:==) CU CD = FalseSym0 type instance (:==) CU CE = FalseSym0 type instance (:==) CU CF = FalseSym0 type instance (:==) CU CG = FalseSym0 type instance (:==) CU CH = FalseSym0 type instance (:==) CU CI = FalseSym0 type instance (:==) CU CJ = FalseSym0 type instance (:==) CU CK = FalseSym0 type instance (:==) CU CL = FalseSym0 type instance (:==) CU CM = FalseSym0 type instance (:==) CU CN = FalseSym0 type instance (:==) CU CO = FalseSym0 type instance (:==) CU CP = FalseSym0 type instance (:==) CU CQ = FalseSym0 type instance (:==) CU CR = FalseSym0 type instance (:==) CU CS = FalseSym0 type instance (:==) CU CT = FalseSym0 type instance (:==) CU CU = TrueSym0 type instance (:==) CU CV = FalseSym0 type instance (:==) CU CW = FalseSym0 type instance (:==) CU CX = FalseSym0 type instance (:==) CU CY = FalseSym0 type instance (:==) CU CZ = FalseSym0 type instance (:==) CV CA = FalseSym0 type instance (:==) CV CB = FalseSym0 type instance (:==) CV CC = FalseSym0 type instance (:==) CV CD = FalseSym0 type instance (:==) CV CE = FalseSym0 type instance (:==) CV CF = FalseSym0 type instance (:==) CV CG = FalseSym0 type instance (:==) CV CH = FalseSym0 type instance (:==) CV CI = FalseSym0 type instance (:==) CV CJ = FalseSym0 type instance (:==) CV CK = FalseSym0 type instance (:==) CV CL = FalseSym0 type instance (:==) CV CM = FalseSym0 type instance (:==) CV CN = FalseSym0 type instance (:==) CV CO = FalseSym0 type instance (:==) CV CP = FalseSym0 type instance (:==) CV CQ = FalseSym0 type instance (:==) CV CR = FalseSym0 type instance (:==) CV CS = FalseSym0 type instance (:==) CV CT = FalseSym0 type instance (:==) CV CU = FalseSym0 type instance (:==) CV CV = TrueSym0 type instance (:==) CV CW = FalseSym0 type instance (:==) CV CX = FalseSym0 type instance (:==) CV CY = FalseSym0 type instance (:==) CV CZ = FalseSym0 type instance (:==) CW CA = FalseSym0 type instance (:==) CW CB = FalseSym0 type instance (:==) CW CC = FalseSym0 type instance (:==) CW CD = FalseSym0 type instance (:==) CW CE = FalseSym0 type instance (:==) CW CF = FalseSym0 type instance (:==) CW CG = FalseSym0 type instance (:==) CW CH = FalseSym0 type instance (:==) CW CI = FalseSym0 type instance (:==) CW CJ = FalseSym0 type instance (:==) CW CK = FalseSym0 type instance (:==) CW CL = FalseSym0 type instance (:==) CW CM = FalseSym0 type instance (:==) CW CN = FalseSym0 type instance (:==) CW CO = FalseSym0 type instance (:==) CW CP = FalseSym0 type instance (:==) CW CQ = FalseSym0 type instance (:==) CW CR = FalseSym0 type instance (:==) CW CS = FalseSym0 type instance (:==) CW CT = FalseSym0 type instance (:==) CW CU = FalseSym0 type instance (:==) CW CV = FalseSym0 type instance (:==) CW CW = TrueSym0 type instance (:==) CW CX = FalseSym0 type instance (:==) CW CY = FalseSym0 type instance (:==) CW CZ = FalseSym0 type instance (:==) CX CA = FalseSym0 type instance (:==) CX CB = FalseSym0 type instance (:==) CX CC = FalseSym0 type instance (:==) CX CD = FalseSym0 type instance (:==) CX CE = FalseSym0 type instance (:==) CX CF = FalseSym0 type instance (:==) CX CG = FalseSym0 type instance (:==) CX CH = FalseSym0 type instance (:==) CX CI = FalseSym0 type instance (:==) CX CJ = FalseSym0 type instance (:==) CX CK = FalseSym0 type instance (:==) CX CL = FalseSym0 type instance (:==) CX CM = FalseSym0 type instance (:==) CX CN = FalseSym0 type instance (:==) CX CO = FalseSym0 type instance (:==) CX CP = FalseSym0 type instance (:==) CX CQ = FalseSym0 type instance (:==) CX CR = FalseSym0 type instance (:==) CX CS = FalseSym0 type instance (:==) CX CT = FalseSym0 type instance (:==) CX CU = FalseSym0 type instance (:==) CX CV = FalseSym0 type instance (:==) CX CW = FalseSym0 type instance (:==) CX CX = TrueSym0 type instance (:==) CX CY = FalseSym0 type instance (:==) CX CZ = FalseSym0 type instance (:==) CY CA = FalseSym0 type instance (:==) CY CB = FalseSym0 type instance (:==) CY CC = FalseSym0 type instance (:==) CY CD = FalseSym0 type instance (:==) CY CE = FalseSym0 type instance (:==) CY CF = FalseSym0 type instance (:==) CY CG = FalseSym0 type instance (:==) CY CH = FalseSym0 type instance (:==) CY CI = FalseSym0 type instance (:==) CY CJ = FalseSym0 type instance (:==) CY CK = FalseSym0 type instance (:==) CY CL = FalseSym0 type instance (:==) CY CM = FalseSym0 type instance (:==) CY CN = FalseSym0 type instance (:==) CY CO = FalseSym0 type instance (:==) CY CP = FalseSym0 type instance (:==) CY CQ = FalseSym0 type instance (:==) CY CR = FalseSym0 type instance (:==) CY CS = FalseSym0 type instance (:==) CY CT = FalseSym0 type instance (:==) CY CU = FalseSym0 type instance (:==) CY CV = FalseSym0 type instance (:==) CY CW = FalseSym0 type instance (:==) CY CX = FalseSym0 type instance (:==) CY CY = TrueSym0 type instance (:==) CY CZ = FalseSym0 type instance (:==) CZ CA = FalseSym0 type instance (:==) CZ CB = FalseSym0 type instance (:==) CZ CC = FalseSym0 type instance (:==) CZ CD = FalseSym0 type instance (:==) CZ CE = FalseSym0 type instance (:==) CZ CF = FalseSym0 type instance (:==) CZ CG = FalseSym0 type instance (:==) CZ CH = FalseSym0 type instance (:==) CZ CI = FalseSym0 type instance (:==) CZ CJ = FalseSym0 type instance (:==) CZ CK = FalseSym0 type instance (:==) CZ CL = FalseSym0 type instance (:==) CZ CM = FalseSym0 type instance (:==) CZ CN = FalseSym0 type instance (:==) CZ CO = FalseSym0 type instance (:==) CZ CP = FalseSym0 type instance (:==) CZ CQ = FalseSym0 type instance (:==) CZ CR = FalseSym0 type instance (:==) CZ CS = FalseSym0 type instance (:==) CZ CT = FalseSym0 type instance (:==) CZ CU = FalseSym0 type instance (:==) CZ CV = FalseSym0 type instance (:==) CZ CW = FalseSym0 type instance (:==) CZ CX = FalseSym0 type instance (:==) CZ CY = FalseSym0 type instance (:==) CZ CZ = TrueSym0 type ACharTyCtor = AChar type ACharTyCtorSym0 = ACharTyCtor 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 AttributeTyCtor = Attribute type AttributeTyCtorSym0 = AttributeTyCtor data AttrSym1 (l :: [AChar]) (l :: TyFun U Attribute) data AttrSym0 (k :: TyFun [AChar] (TyFun U Attribute -> *)) type instance Apply (AttrSym1 a) a = Attr a a type instance Apply AttrSym0 a = AttrSym1 a type SchemaTyCtor = Schema type SchemaTyCtorSym0 = SchemaTyCtor data SchSym0 (k :: TyFun [Attribute] Schema) type instance Apply SchSym0 a = Sch a type family Append (a :: Schema) (a :: Schema) :: Schema type instance Append (Sch s1) (Sch s2) = Apply SchSym0 (Apply (Apply :++$ s1) s2) data AppendSym1 (l :: Schema) (l :: TyFun Schema Schema) data AppendSym0 (k :: TyFun Schema (TyFun Schema Schema -> *)) type instance Apply (AppendSym1 a) a = Append a a type instance Apply AppendSym0 a = AppendSym1 a type family AttrNotIn (a :: Attribute) (a :: Schema) :: Bool type instance AttrNotIn z (Sch GHC.Types.[]) = TrueSym0 type instance AttrNotIn (Attr name u) (Sch (GHC.Types.: (Attr name' z) t)) = Apply (Apply :&&$ (Apply (Apply :/=$ name) name')) (Apply (Apply AttrNotInSym0 (Apply (Apply AttrSym0 name) u)) (Apply SchSym0 t)) data AttrNotInSym1 (l :: Attribute) (l :: TyFun Schema Bool) data AttrNotInSym0 (k :: TyFun Attribute (TyFun Schema Bool -> *)) type instance Apply (AttrNotInSym1 a) a = AttrNotIn a a type instance Apply AttrNotInSym0 a = AttrNotInSym1 a type family Disjoint (a :: Schema) (a :: Schema) :: Bool type instance Disjoint (Sch GHC.Types.[]) z = TrueSym0 type instance Disjoint (Sch (GHC.Types.: h t)) s = Apply (Apply :&&$ (Apply (Apply AttrNotInSym0 h) s)) (Apply (Apply DisjointSym0 (Apply SchSym0 t)) s) data DisjointSym1 (l :: Schema) (l :: TyFun Schema Bool) data DisjointSym0 (k :: TyFun Schema (TyFun Schema Bool -> *)) type instance Apply (DisjointSym1 a) a = Disjoint a a type instance Apply DisjointSym0 a = DisjointSym1 a type family Occurs (a :: [AChar]) (a :: Schema) :: Bool type instance Occurs z (Sch GHC.Types.[]) = FalseSym0 type instance Occurs name (Sch (GHC.Types.: (Attr name' z) attrs)) = Apply (Apply :||$ (Apply (Apply :==$ name) name')) (Apply (Apply OccursSym0 name) (Apply SchSym0 attrs)) data OccursSym1 (l :: [AChar]) (l :: TyFun Schema Bool) data OccursSym0 (k :: TyFun [AChar] (TyFun Schema Bool -> *)) type instance Apply (OccursSym1 a) a = Occurs a a type instance Apply OccursSym0 a = OccursSym1 a type family Lookup (a :: [AChar]) (a :: Schema) :: U type instance Lookup z (Sch GHC.Types.[]) = Any type instance Lookup name (Sch (GHC.Types.: (Attr name' u) attrs)) = If (Apply (Apply :==$ name) name') u (Apply (Apply LookupSym0 name) (Apply SchSym0 attrs)) data LookupSym1 (l :: [AChar]) (l :: TyFun Schema U) data LookupSym0 (k :: TyFun [AChar] (TyFun Schema U -> *)) type instance Apply (LookupSym1 a) a = Lookup a a type instance Apply LookupSym0 a = LookupSym1 a data instance Sing (z :: U) = z ~ BOOL => SBOOL | z ~ STRING => SSTRING | z ~ NAT => SNAT | forall (n :: U) (n :: Nat). z ~ VEC n n => SVEC (Sing n) (Sing n) type SU (z :: U) = Sing z instance SingKind (KProxy :: KProxy U) where type instance DemoteRep (KProxy :: KProxy U) = U fromSing SBOOL = BOOL fromSing SSTRING = STRING fromSing SNAT = NAT fromSing (SVEC b b) = VEC (fromSing b) (fromSing b) toSing BOOL = SomeSing SBOOL toSing STRING = SomeSing SSTRING toSing NAT = SomeSing SNAT toSing (VEC b b) = case (toSing b :: SomeSing (KProxy :: KProxy U), toSing b :: SomeSing (KProxy :: KProxy Nat)) of { (SomeSing c, SomeSing c) -> SomeSing (SVEC c c) } instance SEq (KProxy :: KProxy U) where %:== SBOOL SBOOL = STrue %:== SBOOL SSTRING = SFalse %:== SBOOL SNAT = SFalse %:== SBOOL (SVEC _ _) = SFalse %:== SSTRING SBOOL = SFalse %:== SSTRING SSTRING = STrue %:== SSTRING SNAT = SFalse %:== SSTRING (SVEC _ _) = SFalse %:== SNAT SBOOL = SFalse %:== SNAT SSTRING = SFalse %:== SNAT SNAT = STrue %:== SNAT (SVEC _ _) = SFalse %:== (SVEC _ _) SBOOL = SFalse %:== (SVEC _ _) SSTRING = SFalse %:== (SVEC _ _) SNAT = SFalse %:== (SVEC a a) (SVEC b b) = (%:&&) ((%:==) a b) ((%:==) a b) instance SDecide (KProxy :: KProxy U) where %~ SBOOL SBOOL = Proved Refl %~ SBOOL SSTRING = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SBOOL SNAT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SBOOL (SVEC _ _) = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SSTRING SBOOL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SSTRING SSTRING = Proved Refl %~ SSTRING SNAT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SSTRING (SVEC _ _) = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SNAT SBOOL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SNAT SSTRING = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SNAT SNAT = Proved Refl %~ SNAT (SVEC _ _) = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ (SVEC _ _) SBOOL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ (SVEC _ _) SSTRING = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ (SVEC _ _) SNAT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ (SVEC a a) (SVEC b b) = case ((%~) a b, (%~) a b) of { (Proved Refl, Proved Refl) -> Proved Refl (Disproved contra, _) -> Disproved (\ Refl -> contra Refl) (_, Disproved contra) -> Disproved (\ Refl -> contra Refl) } instance SingI BOOL where sing = SBOOL instance SingI STRING where sing = SSTRING instance SingI NAT where sing = SNAT instance (SingI n, SingI n) => SingI (VEC (n :: U) (n :: Nat)) where sing = SVEC sing sing data instance Sing (z :: AChar) = z ~ CA => SCA | z ~ CB => SCB | z ~ CC => SCC | z ~ CD => SCD | z ~ CE => SCE | z ~ CF => SCF | z ~ CG => SCG | z ~ CH => SCH | z ~ CI => SCI | z ~ CJ => SCJ | z ~ CK => SCK | z ~ CL => SCL | z ~ CM => SCM | z ~ CN => SCN | z ~ CO => SCO | z ~ CP => SCP | z ~ CQ => SCQ | z ~ CR => SCR | z ~ CS => SCS | z ~ CT => SCT | z ~ CU => SCU | z ~ CV => SCV | z ~ CW => SCW | z ~ CX => SCX | z ~ CY => SCY | z ~ CZ => SCZ type SAChar (z :: AChar) = Sing z instance SingKind (KProxy :: KProxy AChar) where type instance DemoteRep (KProxy :: KProxy AChar) = AChar fromSing SCA = CA fromSing SCB = CB fromSing SCC = CC fromSing SCD = CD fromSing SCE = CE fromSing SCF = CF fromSing SCG = CG fromSing SCH = CH fromSing SCI = CI fromSing SCJ = CJ fromSing SCK = CK fromSing SCL = CL fromSing SCM = CM fromSing SCN = CN fromSing SCO = CO fromSing SCP = CP fromSing SCQ = CQ fromSing SCR = CR fromSing SCS = CS fromSing SCT = CT fromSing SCU = CU fromSing SCV = CV fromSing SCW = CW fromSing SCX = CX fromSing SCY = CY fromSing SCZ = CZ toSing CA = SomeSing SCA toSing CB = SomeSing SCB toSing CC = SomeSing SCC toSing CD = SomeSing SCD toSing CE = SomeSing SCE toSing CF = SomeSing SCF toSing CG = SomeSing SCG toSing CH = SomeSing SCH toSing CI = SomeSing SCI toSing CJ = SomeSing SCJ toSing CK = SomeSing SCK toSing CL = SomeSing SCL toSing CM = SomeSing SCM toSing CN = SomeSing SCN toSing CO = SomeSing SCO toSing CP = SomeSing SCP toSing CQ = SomeSing SCQ toSing CR = SomeSing SCR toSing CS = SomeSing SCS toSing CT = SomeSing SCT toSing CU = SomeSing SCU toSing CV = SomeSing SCV toSing CW = SomeSing SCW toSing CX = SomeSing SCX toSing CY = SomeSing SCY toSing CZ = SomeSing SCZ instance SEq (KProxy :: KProxy AChar) where %:== SCA SCA = STrue %:== SCA SCB = SFalse %:== SCA SCC = SFalse %:== SCA SCD = SFalse %:== SCA SCE = SFalse %:== SCA SCF = SFalse %:== SCA SCG = SFalse %:== SCA SCH = SFalse %:== SCA SCI = SFalse %:== SCA SCJ = SFalse %:== SCA SCK = SFalse %:== SCA SCL = SFalse %:== SCA SCM = SFalse %:== SCA SCN = SFalse %:== SCA SCO = SFalse %:== SCA SCP = SFalse %:== SCA SCQ = SFalse %:== SCA SCR = SFalse %:== SCA SCS = SFalse %:== SCA SCT = SFalse %:== SCA SCU = SFalse %:== SCA SCV = SFalse %:== SCA SCW = SFalse %:== SCA SCX = SFalse %:== SCA SCY = SFalse %:== SCA SCZ = SFalse %:== SCB SCA = SFalse %:== SCB SCB = STrue %:== SCB SCC = SFalse %:== SCB SCD = SFalse %:== SCB SCE = SFalse %:== SCB SCF = SFalse %:== SCB SCG = SFalse %:== SCB SCH = SFalse %:== SCB SCI = SFalse %:== SCB SCJ = SFalse %:== SCB SCK = SFalse %:== SCB SCL = SFalse %:== SCB SCM = SFalse %:== SCB SCN = SFalse %:== SCB SCO = SFalse %:== SCB SCP = SFalse %:== SCB SCQ = SFalse %:== SCB SCR = SFalse %:== SCB SCS = SFalse %:== SCB SCT = SFalse %:== SCB SCU = SFalse %:== SCB SCV = SFalse %:== SCB SCW = SFalse %:== SCB SCX = SFalse %:== SCB SCY = SFalse %:== SCB SCZ = SFalse %:== SCC SCA = SFalse %:== SCC SCB = SFalse %:== SCC SCC = STrue %:== SCC SCD = SFalse %:== SCC SCE = SFalse %:== SCC SCF = SFalse %:== SCC SCG = SFalse %:== SCC SCH = SFalse %:== SCC SCI = SFalse %:== SCC SCJ = SFalse %:== SCC SCK = SFalse %:== SCC SCL = SFalse %:== SCC SCM = SFalse %:== SCC SCN = SFalse %:== SCC SCO = SFalse %:== SCC SCP = SFalse %:== SCC SCQ = SFalse %:== SCC SCR = SFalse %:== SCC SCS = SFalse %:== SCC SCT = SFalse %:== SCC SCU = SFalse %:== SCC SCV = SFalse %:== SCC SCW = SFalse %:== SCC SCX = SFalse %:== SCC SCY = SFalse %:== SCC SCZ = SFalse %:== SCD SCA = SFalse %:== SCD SCB = SFalse %:== SCD SCC = SFalse %:== SCD SCD = STrue %:== SCD SCE = SFalse %:== SCD SCF = SFalse %:== SCD SCG = SFalse %:== SCD SCH = SFalse %:== SCD SCI = SFalse %:== SCD SCJ = SFalse %:== SCD SCK = SFalse %:== SCD SCL = SFalse %:== SCD SCM = SFalse %:== SCD SCN = SFalse %:== SCD SCO = SFalse %:== SCD SCP = SFalse %:== SCD SCQ = SFalse %:== SCD SCR = SFalse %:== SCD SCS = SFalse %:== SCD SCT = SFalse %:== SCD SCU = SFalse %:== SCD SCV = SFalse %:== SCD SCW = SFalse %:== SCD SCX = SFalse %:== SCD SCY = SFalse %:== SCD SCZ = SFalse %:== SCE SCA = SFalse %:== SCE SCB = SFalse %:== SCE SCC = SFalse %:== SCE SCD = SFalse %:== SCE SCE = STrue %:== SCE SCF = SFalse %:== SCE SCG = SFalse %:== SCE SCH = SFalse %:== SCE SCI = SFalse %:== SCE SCJ = SFalse %:== SCE SCK = SFalse %:== SCE SCL = SFalse %:== SCE SCM = SFalse %:== SCE SCN = SFalse %:== SCE SCO = SFalse %:== SCE SCP = SFalse %:== SCE SCQ = SFalse %:== SCE SCR = SFalse %:== SCE SCS = SFalse %:== SCE SCT = SFalse %:== SCE SCU = SFalse %:== SCE SCV = SFalse %:== SCE SCW = SFalse %:== SCE SCX = SFalse %:== SCE SCY = SFalse %:== SCE SCZ = SFalse %:== SCF SCA = SFalse %:== SCF SCB = SFalse %:== SCF SCC = SFalse %:== SCF SCD = SFalse %:== SCF SCE = SFalse %:== SCF SCF = STrue %:== SCF SCG = SFalse %:== SCF SCH = SFalse %:== SCF SCI = SFalse %:== SCF SCJ = SFalse %:== SCF SCK = SFalse %:== SCF SCL = SFalse %:== SCF SCM = SFalse %:== SCF SCN = SFalse %:== SCF SCO = SFalse %:== SCF SCP = SFalse %:== SCF SCQ = SFalse %:== SCF SCR = SFalse %:== SCF SCS = SFalse %:== SCF SCT = SFalse %:== SCF SCU = SFalse %:== SCF SCV = SFalse %:== SCF SCW = SFalse %:== SCF SCX = SFalse %:== SCF SCY = SFalse %:== SCF SCZ = SFalse %:== SCG SCA = SFalse %:== SCG SCB = SFalse %:== SCG SCC = SFalse %:== SCG SCD = SFalse %:== SCG SCE = SFalse %:== SCG SCF = SFalse %:== SCG SCG = STrue %:== SCG SCH = SFalse %:== SCG SCI = SFalse %:== SCG SCJ = SFalse %:== SCG SCK = SFalse %:== SCG SCL = SFalse %:== SCG SCM = SFalse %:== SCG SCN = SFalse %:== SCG SCO = SFalse %:== SCG SCP = SFalse %:== SCG SCQ = SFalse %:== SCG SCR = SFalse %:== SCG SCS = SFalse %:== SCG SCT = SFalse %:== SCG SCU = SFalse %:== SCG SCV = SFalse %:== SCG SCW = SFalse %:== SCG SCX = SFalse %:== SCG SCY = SFalse %:== SCG SCZ = SFalse %:== SCH SCA = SFalse %:== SCH SCB = SFalse %:== SCH SCC = SFalse %:== SCH SCD = SFalse %:== SCH SCE = SFalse %:== SCH SCF = SFalse %:== SCH SCG = SFalse %:== SCH SCH = STrue %:== SCH SCI = SFalse %:== SCH SCJ = SFalse %:== SCH SCK = SFalse %:== SCH SCL = SFalse %:== SCH SCM = SFalse %:== SCH SCN = SFalse %:== SCH SCO = SFalse %:== SCH SCP = SFalse %:== SCH SCQ = SFalse %:== SCH SCR = SFalse %:== SCH SCS = SFalse %:== SCH SCT = SFalse %:== SCH SCU = SFalse %:== SCH SCV = SFalse %:== SCH SCW = SFalse %:== SCH SCX = SFalse %:== SCH SCY = SFalse %:== SCH SCZ = SFalse %:== SCI SCA = SFalse %:== SCI SCB = SFalse %:== SCI SCC = SFalse %:== SCI SCD = SFalse %:== SCI SCE = SFalse %:== SCI SCF = SFalse %:== SCI SCG = SFalse %:== SCI SCH = SFalse %:== SCI SCI = STrue %:== SCI SCJ = SFalse %:== SCI SCK = SFalse %:== SCI SCL = SFalse %:== SCI SCM = SFalse %:== SCI SCN = SFalse %:== SCI SCO = SFalse %:== SCI SCP = SFalse %:== SCI SCQ = SFalse %:== SCI SCR = SFalse %:== SCI SCS = SFalse %:== SCI SCT = SFalse %:== SCI SCU = SFalse %:== SCI SCV = SFalse %:== SCI SCW = SFalse %:== SCI SCX = SFalse %:== SCI SCY = SFalse %:== SCI SCZ = SFalse %:== SCJ SCA = SFalse %:== SCJ SCB = SFalse %:== SCJ SCC = SFalse %:== SCJ SCD = SFalse %:== SCJ SCE = SFalse %:== SCJ SCF = SFalse %:== SCJ SCG = SFalse %:== SCJ SCH = SFalse %:== SCJ SCI = SFalse %:== SCJ SCJ = STrue %:== SCJ SCK = SFalse %:== SCJ SCL = SFalse %:== SCJ SCM = SFalse %:== SCJ SCN = SFalse %:== SCJ SCO = SFalse %:== SCJ SCP = SFalse %:== SCJ SCQ = SFalse %:== SCJ SCR = SFalse %:== SCJ SCS = SFalse %:== SCJ SCT = SFalse %:== SCJ SCU = SFalse %:== SCJ SCV = SFalse %:== SCJ SCW = SFalse %:== SCJ SCX = SFalse %:== SCJ SCY = SFalse %:== SCJ SCZ = SFalse %:== SCK SCA = SFalse %:== SCK SCB = SFalse %:== SCK SCC = SFalse %:== SCK SCD = SFalse %:== SCK SCE = SFalse %:== SCK SCF = SFalse %:== SCK SCG = SFalse %:== SCK SCH = SFalse %:== SCK SCI = SFalse %:== SCK SCJ = SFalse %:== SCK SCK = STrue %:== SCK SCL = SFalse %:== SCK SCM = SFalse %:== SCK SCN = SFalse %:== SCK SCO = SFalse %:== SCK SCP = SFalse %:== SCK SCQ = SFalse %:== SCK SCR = SFalse %:== SCK SCS = SFalse %:== SCK SCT = SFalse %:== SCK SCU = SFalse %:== SCK SCV = SFalse %:== SCK SCW = SFalse %:== SCK SCX = SFalse %:== SCK SCY = SFalse %:== SCK SCZ = SFalse %:== SCL SCA = SFalse %:== SCL SCB = SFalse %:== SCL SCC = SFalse %:== SCL SCD = SFalse %:== SCL SCE = SFalse %:== SCL SCF = SFalse %:== SCL SCG = SFalse %:== SCL SCH = SFalse %:== SCL SCI = SFalse %:== SCL SCJ = SFalse %:== SCL SCK = SFalse %:== SCL SCL = STrue %:== SCL SCM = SFalse %:== SCL SCN = SFalse %:== SCL SCO = SFalse %:== SCL SCP = SFalse %:== SCL SCQ = SFalse %:== SCL SCR = SFalse %:== SCL SCS = SFalse %:== SCL SCT = SFalse %:== SCL SCU = SFalse %:== SCL SCV = SFalse %:== SCL SCW = SFalse %:== SCL SCX = SFalse %:== SCL SCY = SFalse %:== SCL SCZ = SFalse %:== SCM SCA = SFalse %:== SCM SCB = SFalse %:== SCM SCC = SFalse %:== SCM SCD = SFalse %:== SCM SCE = SFalse %:== SCM SCF = SFalse %:== SCM SCG = SFalse %:== SCM SCH = SFalse %:== SCM SCI = SFalse %:== SCM SCJ = SFalse %:== SCM SCK = SFalse %:== SCM SCL = SFalse %:== SCM SCM = STrue %:== SCM SCN = SFalse %:== SCM SCO = SFalse %:== SCM SCP = SFalse %:== SCM SCQ = SFalse %:== SCM SCR = SFalse %:== SCM SCS = SFalse %:== SCM SCT = SFalse %:== SCM SCU = SFalse %:== SCM SCV = SFalse %:== SCM SCW = SFalse %:== SCM SCX = SFalse %:== SCM SCY = SFalse %:== SCM SCZ = SFalse %:== SCN SCA = SFalse %:== SCN SCB = SFalse %:== SCN SCC = SFalse %:== SCN SCD = SFalse %:== SCN SCE = SFalse %:== SCN SCF = SFalse %:== SCN SCG = SFalse %:== SCN SCH = SFalse %:== SCN SCI = SFalse %:== SCN SCJ = SFalse %:== SCN SCK = SFalse %:== SCN SCL = SFalse %:== SCN SCM = SFalse %:== SCN SCN = STrue %:== SCN SCO = SFalse %:== SCN SCP = SFalse %:== SCN SCQ = SFalse %:== SCN SCR = SFalse %:== SCN SCS = SFalse %:== SCN SCT = SFalse %:== SCN SCU = SFalse %:== SCN SCV = SFalse %:== SCN SCW = SFalse %:== SCN SCX = SFalse %:== SCN SCY = SFalse %:== SCN SCZ = SFalse %:== SCO SCA = SFalse %:== SCO SCB = SFalse %:== SCO SCC = SFalse %:== SCO SCD = SFalse %:== SCO SCE = SFalse %:== SCO SCF = SFalse %:== SCO SCG = SFalse %:== SCO SCH = SFalse %:== SCO SCI = SFalse %:== SCO SCJ = SFalse %:== SCO SCK = SFalse %:== SCO SCL = SFalse %:== SCO SCM = SFalse %:== SCO SCN = SFalse %:== SCO SCO = STrue %:== SCO SCP = SFalse %:== SCO SCQ = SFalse %:== SCO SCR = SFalse %:== SCO SCS = SFalse %:== SCO SCT = SFalse %:== SCO SCU = SFalse %:== SCO SCV = SFalse %:== SCO SCW = SFalse %:== SCO SCX = SFalse %:== SCO SCY = SFalse %:== SCO SCZ = SFalse %:== SCP SCA = SFalse %:== SCP SCB = SFalse %:== SCP SCC = SFalse %:== SCP SCD = SFalse %:== SCP SCE = SFalse %:== SCP SCF = SFalse %:== SCP SCG = SFalse %:== SCP SCH = SFalse %:== SCP SCI = SFalse %:== SCP SCJ = SFalse %:== SCP SCK = SFalse %:== SCP SCL = SFalse %:== SCP SCM = SFalse %:== SCP SCN = SFalse %:== SCP SCO = SFalse %:== SCP SCP = STrue %:== SCP SCQ = SFalse %:== SCP SCR = SFalse %:== SCP SCS = SFalse %:== SCP SCT = SFalse %:== SCP SCU = SFalse %:== SCP SCV = SFalse %:== SCP SCW = SFalse %:== SCP SCX = SFalse %:== SCP SCY = SFalse %:== SCP SCZ = SFalse %:== SCQ SCA = SFalse %:== SCQ SCB = SFalse %:== SCQ SCC = SFalse %:== SCQ SCD = SFalse %:== SCQ SCE = SFalse %:== SCQ SCF = SFalse %:== SCQ SCG = SFalse %:== SCQ SCH = SFalse %:== SCQ SCI = SFalse %:== SCQ SCJ = SFalse %:== SCQ SCK = SFalse %:== SCQ SCL = SFalse %:== SCQ SCM = SFalse %:== SCQ SCN = SFalse %:== SCQ SCO = SFalse %:== SCQ SCP = SFalse %:== SCQ SCQ = STrue %:== SCQ SCR = SFalse %:== SCQ SCS = SFalse %:== SCQ SCT = SFalse %:== SCQ SCU = SFalse %:== SCQ SCV = SFalse %:== SCQ SCW = SFalse %:== SCQ SCX = SFalse %:== SCQ SCY = SFalse %:== SCQ SCZ = SFalse %:== SCR SCA = SFalse %:== SCR SCB = SFalse %:== SCR SCC = SFalse %:== SCR SCD = SFalse %:== SCR SCE = SFalse %:== SCR SCF = SFalse %:== SCR SCG = SFalse %:== SCR SCH = SFalse %:== SCR SCI = SFalse %:== SCR SCJ = SFalse %:== SCR SCK = SFalse %:== SCR SCL = SFalse %:== SCR SCM = SFalse %:== SCR SCN = SFalse %:== SCR SCO = SFalse %:== SCR SCP = SFalse %:== SCR SCQ = SFalse %:== SCR SCR = STrue %:== SCR SCS = SFalse %:== SCR SCT = SFalse %:== SCR SCU = SFalse %:== SCR SCV = SFalse %:== SCR SCW = SFalse %:== SCR SCX = SFalse %:== SCR SCY = SFalse %:== SCR SCZ = SFalse %:== SCS SCA = SFalse %:== SCS SCB = SFalse %:== SCS SCC = SFalse %:== SCS SCD = SFalse %:== SCS SCE = SFalse %:== SCS SCF = SFalse %:== SCS SCG = SFalse %:== SCS SCH = SFalse %:== SCS SCI = SFalse %:== SCS SCJ = SFalse %:== SCS SCK = SFalse %:== SCS SCL = SFalse %:== SCS SCM = SFalse %:== SCS SCN = SFalse %:== SCS SCO = SFalse %:== SCS SCP = SFalse %:== SCS SCQ = SFalse %:== SCS SCR = SFalse %:== SCS SCS = STrue %:== SCS SCT = SFalse %:== SCS SCU = SFalse %:== SCS SCV = SFalse %:== SCS SCW = SFalse %:== SCS SCX = SFalse %:== SCS SCY = SFalse %:== SCS SCZ = SFalse %:== SCT SCA = SFalse %:== SCT SCB = SFalse %:== SCT SCC = SFalse %:== SCT SCD = SFalse %:== SCT SCE = SFalse %:== SCT SCF = SFalse %:== SCT SCG = SFalse %:== SCT SCH = SFalse %:== SCT SCI = SFalse %:== SCT SCJ = SFalse %:== SCT SCK = SFalse %:== SCT SCL = SFalse %:== SCT SCM = SFalse %:== SCT SCN = SFalse %:== SCT SCO = SFalse %:== SCT SCP = SFalse %:== SCT SCQ = SFalse %:== SCT SCR = SFalse %:== SCT SCS = SFalse %:== SCT SCT = STrue %:== SCT SCU = SFalse %:== SCT SCV = SFalse %:== SCT SCW = SFalse %:== SCT SCX = SFalse %:== SCT SCY = SFalse %:== SCT SCZ = SFalse %:== SCU SCA = SFalse %:== SCU SCB = SFalse %:== SCU SCC = SFalse %:== SCU SCD = SFalse %:== SCU SCE = SFalse %:== SCU SCF = SFalse %:== SCU SCG = SFalse %:== SCU SCH = SFalse %:== SCU SCI = SFalse %:== SCU SCJ = SFalse %:== SCU SCK = SFalse %:== SCU SCL = SFalse %:== SCU SCM = SFalse %:== SCU SCN = SFalse %:== SCU SCO = SFalse %:== SCU SCP = SFalse %:== SCU SCQ = SFalse %:== SCU SCR = SFalse %:== SCU SCS = SFalse %:== SCU SCT = SFalse %:== SCU SCU = STrue %:== SCU SCV = SFalse %:== SCU SCW = SFalse %:== SCU SCX = SFalse %:== SCU SCY = SFalse %:== SCU SCZ = SFalse %:== SCV SCA = SFalse %:== SCV SCB = SFalse %:== SCV SCC = SFalse %:== SCV SCD = SFalse %:== SCV SCE = SFalse %:== SCV SCF = SFalse %:== SCV SCG = SFalse %:== SCV SCH = SFalse %:== SCV SCI = SFalse %:== SCV SCJ = SFalse %:== SCV SCK = SFalse %:== SCV SCL = SFalse %:== SCV SCM = SFalse %:== SCV SCN = SFalse %:== SCV SCO = SFalse %:== SCV SCP = SFalse %:== SCV SCQ = SFalse %:== SCV SCR = SFalse %:== SCV SCS = SFalse %:== SCV SCT = SFalse %:== SCV SCU = SFalse %:== SCV SCV = STrue %:== SCV SCW = SFalse %:== SCV SCX = SFalse %:== SCV SCY = SFalse %:== SCV SCZ = SFalse %:== SCW SCA = SFalse %:== SCW SCB = SFalse %:== SCW SCC = SFalse %:== SCW SCD = SFalse %:== SCW SCE = SFalse %:== SCW SCF = SFalse %:== SCW SCG = SFalse %:== SCW SCH = SFalse %:== SCW SCI = SFalse %:== SCW SCJ = SFalse %:== SCW SCK = SFalse %:== SCW SCL = SFalse %:== SCW SCM = SFalse %:== SCW SCN = SFalse %:== SCW SCO = SFalse %:== SCW SCP = SFalse %:== SCW SCQ = SFalse %:== SCW SCR = SFalse %:== SCW SCS = SFalse %:== SCW SCT = SFalse %:== SCW SCU = SFalse %:== SCW SCV = SFalse %:== SCW SCW = STrue %:== SCW SCX = SFalse %:== SCW SCY = SFalse %:== SCW SCZ = SFalse %:== SCX SCA = SFalse %:== SCX SCB = SFalse %:== SCX SCC = SFalse %:== SCX SCD = SFalse %:== SCX SCE = SFalse %:== SCX SCF = SFalse %:== SCX SCG = SFalse %:== SCX SCH = SFalse %:== SCX SCI = SFalse %:== SCX SCJ = SFalse %:== SCX SCK = SFalse %:== SCX SCL = SFalse %:== SCX SCM = SFalse %:== SCX SCN = SFalse %:== SCX SCO = SFalse %:== SCX SCP = SFalse %:== SCX SCQ = SFalse %:== SCX SCR = SFalse %:== SCX SCS = SFalse %:== SCX SCT = SFalse %:== SCX SCU = SFalse %:== SCX SCV = SFalse %:== SCX SCW = SFalse %:== SCX SCX = STrue %:== SCX SCY = SFalse %:== SCX SCZ = SFalse %:== SCY SCA = SFalse %:== SCY SCB = SFalse %:== SCY SCC = SFalse %:== SCY SCD = SFalse %:== SCY SCE = SFalse %:== SCY SCF = SFalse %:== SCY SCG = SFalse %:== SCY SCH = SFalse %:== SCY SCI = SFalse %:== SCY SCJ = SFalse %:== SCY SCK = SFalse %:== SCY SCL = SFalse %:== SCY SCM = SFalse %:== SCY SCN = SFalse %:== SCY SCO = SFalse %:== SCY SCP = SFalse %:== SCY SCQ = SFalse %:== SCY SCR = SFalse %:== SCY SCS = SFalse %:== SCY SCT = SFalse %:== SCY SCU = SFalse %:== SCY SCV = SFalse %:== SCY SCW = SFalse %:== SCY SCX = SFalse %:== SCY SCY = STrue %:== SCY SCZ = SFalse %:== SCZ SCA = SFalse %:== SCZ SCB = SFalse %:== SCZ SCC = SFalse %:== SCZ SCD = SFalse %:== SCZ SCE = SFalse %:== SCZ SCF = SFalse %:== SCZ SCG = SFalse %:== SCZ SCH = SFalse %:== SCZ SCI = SFalse %:== SCZ SCJ = SFalse %:== SCZ SCK = SFalse %:== SCZ SCL = SFalse %:== SCZ SCM = SFalse %:== SCZ SCN = SFalse %:== SCZ SCO = SFalse %:== SCZ SCP = SFalse %:== SCZ SCQ = SFalse %:== SCZ SCR = SFalse %:== SCZ SCS = SFalse %:== SCZ SCT = SFalse %:== SCZ SCU = SFalse %:== SCZ SCV = SFalse %:== SCZ SCW = SFalse %:== SCZ SCX = SFalse %:== SCZ SCY = SFalse %:== SCZ SCZ = STrue instance SDecide (KProxy :: KProxy AChar) where %~ SCA SCA = Proved Refl %~ SCA SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCA SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCB = Proved Refl %~ SCB SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCB SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCC = Proved Refl %~ SCC SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCC SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCD = Proved Refl %~ SCD SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCD SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCE = Proved Refl %~ SCE SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCE SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCF = Proved Refl %~ SCF SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCF SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCG = Proved Refl %~ SCG SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCG SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCH = Proved Refl %~ SCH SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCH SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCI = Proved Refl %~ SCI SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCI SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCJ = Proved Refl %~ SCJ SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCJ SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCK = Proved Refl %~ SCK SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCK SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCL = Proved Refl %~ SCL SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCL SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCM = Proved Refl %~ SCM SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCM SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCN = Proved Refl %~ SCN SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCN SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCO = Proved Refl %~ SCO SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCO SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCP = Proved Refl %~ SCP SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCP SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCQ = Proved Refl %~ SCQ SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCQ SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCR = Proved Refl %~ SCR SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCR SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCS = Proved Refl %~ SCS SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCS SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCT = Proved Refl %~ SCT SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCT SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCU = Proved Refl %~ SCU SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCU SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCV = Proved Refl %~ SCV SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCV SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCW = Proved Refl %~ SCW SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCW SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCX = Proved Refl %~ SCX SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCX SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCY SCY = Proved Refl %~ SCY SCZ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCA = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCB = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCC = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCD = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCE = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCF = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCG = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCH = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCI = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCJ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCK = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCL = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCM = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCN = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCO = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCP = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCQ = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCR = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCS = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCT = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCU = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCV = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCW = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCX = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCY = Disproved (\case { _ -> error "Empty case reached -- this should be impossible" }) %~ SCZ SCZ = Proved Refl instance SingI CA where sing = SCA instance SingI CB where sing = SCB instance SingI CC where sing = SCC instance SingI CD where sing = SCD instance SingI CE where sing = SCE instance SingI CF where sing = SCF instance SingI CG where sing = SCG instance SingI CH where sing = SCH instance SingI CI where sing = SCI instance SingI CJ where sing = SCJ instance SingI CK where sing = SCK instance SingI CL where sing = SCL instance SingI CM where sing = SCM instance SingI CN where sing = SCN instance SingI CO where sing = SCO instance SingI CP where sing = SCP instance SingI CQ where sing = SCQ instance SingI CR where sing = SCR instance SingI CS where sing = SCS instance SingI CT where sing = SCT instance SingI CU where sing = SCU instance SingI CV where sing = SCV instance SingI CW where sing = SCW instance SingI CX where sing = SCX instance SingI CY where sing = SCY instance SingI CZ where sing = SCZ data instance Sing (z :: Attribute) = forall (n :: [AChar]) (n :: U). z ~ Attr n n => SAttr (Sing n) (Sing n) type SAttribute (z :: Attribute) = Sing z instance SingKind (KProxy :: KProxy Attribute) where type instance DemoteRep (KProxy :: KProxy Attribute) = Attribute fromSing (SAttr b b) = Attr (fromSing b) (fromSing b) toSing (Attr b b) = case (toSing b :: SomeSing (KProxy :: KProxy [AChar]), toSing b :: SomeSing (KProxy :: KProxy U)) of { (SomeSing c, SomeSing c) -> SomeSing (SAttr c c) } instance (SingI n, SingI n) => SingI (Attr (n :: [AChar]) (n :: U)) where sing = SAttr sing sing data instance Sing (z :: Schema) = forall (n :: [Attribute]). z ~ Sch n => SSch (Sing n) type SSchema (z :: Schema) = Sing z instance SingKind (KProxy :: KProxy Schema) where type instance DemoteRep (KProxy :: KProxy Schema) = Schema fromSing (SSch b) = Sch (fromSing b) toSing (Sch b) = case toSing b :: SomeSing (KProxy :: KProxy [Attribute]) of { SomeSing c -> SomeSing (SSch c) } instance SingI n => SingI (Sch (n :: [Attribute])) where sing = SSch sing sAppend :: forall (t :: Schema) (t :: Schema). Sing t -> Sing t -> Sing (Append t t) sAppend (SSch s1) (SSch s2) = SSch ((%:++) s1 s2) sAttrNotIn :: forall (t :: Attribute) (t :: Schema). Sing t -> Sing t -> Sing (AttrNotIn t t) sAttrNotIn _ (SSch SNil) = STrue sAttrNotIn (SAttr name u) (SSch (SCons (SAttr name' _) t)) = (%:&&) ((%:/=) name name') (sAttrNotIn (SAttr name u) (SSch t)) sDisjoint :: forall (t :: Schema) (t :: Schema). Sing t -> Sing t -> Sing (Disjoint t t) sDisjoint (SSch SNil) _ = STrue sDisjoint (SSch (SCons h t)) s = (%:&&) (sAttrNotIn h s) (sDisjoint (SSch t) s) sOccurs :: forall (t :: [AChar]) (t :: Schema). Sing t -> Sing t -> Sing (Occurs t t) sOccurs _ (SSch SNil) = SFalse sOccurs name (SSch (SCons (SAttr name' _) attrs)) = (%:||) ((%:==) name name') (sOccurs name (SSch attrs)) sLookup :: forall (t :: [AChar]) (t :: Schema). Sing t -> Sing t -> Sing (Lookup t t) sLookup _ (SSch SNil) = undefined sLookup name (SSch (SCons (SAttr name' u) attrs)) = sIf ((%:==) name name') u (sLookup name (SSch attrs)) GradingClient/Database.hs:0:0: Splicing declarations return [] ======> GradingClient/Database.hs:0:0: GradingClient/Database.hs:(0,0)-(0,0): Splicing expression cases ''Row [| r |] [| changeId (n ++ (getId r)) r |] ======> case r of { EmptyRow _ -> changeId (n ++ (getId r)) r ConsRow _ _ -> changeId (n ++ (getId r)) r }