GradingClient/Database.hs:0:0: Splicing declarations singletons [d| data Nat = Zero | Succ Nat deriving (Eq, Ord) |] ======> GradingClient/Database.hs:(0,0)-(0,0) data Nat = Zero | Succ Nat deriving (Eq, Ord) type family Equals_0123456789 (a :: Nat) (b :: Nat) :: Bool where Equals_0123456789 Zero Zero = TrueSym0 Equals_0123456789 (Succ a) (Succ b) = (:==) a b Equals_0123456789 (a :: Nat) (b :: Nat) = FalseSym0 instance PEq (KProxy :: KProxy Nat) where type (:==) (a :: Nat) (b :: Nat) = Equals_0123456789 a b instance POrd (KProxy :: KProxy Nat) where type Compare Zero Zero = EQ type Compare Zero (Succ rhs) = LT type Compare (Succ lhs) Zero = GT type Compare (Succ lhs) (Succ rhs) = ThenCmp EQ (Compare lhs rhs) type ZeroSym0 = Zero type SuccSym1 (t :: Nat) = Succ t instance SuppressUnusedWarnings SuccSym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) SuccSym0KindInference GHC.Tuple.()) data SuccSym0 (l :: TyFun Nat Nat) = forall arg. KindOf (Apply SuccSym0 arg) ~ KindOf (SuccSym1 arg) => SuccSym0KindInference type instance Apply SuccSym0 l = SuccSym1 l data instance Sing (z :: Nat) = z ~ Zero => SZero | forall (n :: Nat). z ~ Succ n => SSucc (Sing n) type SNat (z :: Nat) = Sing z instance SingKind (KProxy :: KProxy Nat) where type DemoteRep (KProxy :: KProxy Nat) = Nat fromSing SZero = Zero fromSing (SSucc b) = Succ (fromSing b) toSing Zero = SomeSing SZero toSing (Succ b) = case toSing b :: SomeSing (KProxy :: KProxy Nat) of { SomeSing c -> SomeSing (SSucc c) } instance SEq (KProxy :: KProxy Nat) where (%:==) SZero SZero = STrue (%:==) SZero (SSucc _) = SFalse (%:==) (SSucc _) SZero = SFalse (%:==) (SSucc a) (SSucc b) = (%:==) a b instance SDecide (KProxy :: KProxy Nat) where (%~) SZero SZero = Proved Refl (%~) SZero (SSucc _) = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) (SSucc _) SZero = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) (SSucc a) (SSucc b) = case (%~) a b of { Proved Refl -> Proved Refl Disproved contra -> Disproved (\ refl -> case refl of { Refl -> contra Refl }) } instance SingI Zero where sing = SZero instance SingI n => SingI (Succ (n :: Nat)) where sing = SSucc sing GradingClient/Database.hs:0:0: Splicing declarations singletons [d| append :: Schema -> Schema -> Schema append (Sch s1) (Sch s2) = Sch (s1 ++ s2) attrNotIn :: Attribute -> Schema -> Bool attrNotIn _ (Sch []) = True attrNotIn (Attr name u) (Sch ((Attr name' _) : t)) = (name /= name') && (attrNotIn (Attr name u) (Sch t)) disjoint :: Schema -> Schema -> Bool disjoint (Sch []) _ = True disjoint (Sch (h : t)) s = (attrNotIn h s) && (disjoint (Sch t) s) occurs :: [AChar] -> Schema -> Bool occurs _ (Sch []) = False occurs name (Sch ((Attr name' _) : attrs)) = name == name' || occurs name (Sch attrs) lookup :: [AChar] -> Schema -> U lookup _ (Sch []) = undefined lookup name (Sch ((Attr name' u) : attrs)) = if name == name' then u else lookup name (Sch attrs) data U = BOOL | STRING | NAT | VEC U Nat deriving (Read, Eq, Show) data AChar = CA | CB | CC | CD | CE | CF | CG | CH | CI | CJ | CK | CL | CM | CN | CO | CP | CQ | CR | CS | CT | CU | CV | CW | CX | CY | CZ deriving (Read, Show, Eq) data Attribute = Attr [AChar] U data Schema = Sch [Attribute] |] ======> GradingClient/Database.hs:(0,0)-(0,0) data U = BOOL | STRING | NAT | VEC U Nat deriving (Read, Eq, Show) data AChar = CA | CB | CC | CD | CE | CF | CG | CH | CI | CJ | CK | CL | CM | CN | CO | CP | CQ | CR | CS | CT | CU | CV | CW | CX | CY | CZ deriving (Read, Show, Eq) data Attribute = Attr [AChar] U data Schema = Sch [Attribute] append :: Schema -> Schema -> Schema append (Sch s1) (Sch s2) = Sch (s1 ++ s2) attrNotIn :: Attribute -> Schema -> Bool attrNotIn _ (Sch GHC.Types.[]) = True attrNotIn (Attr name u) (Sch ((Attr name' _) GHC.Types.: t)) = ((name /= name') && (attrNotIn (Attr name u) (Sch t))) disjoint :: Schema -> Schema -> Bool disjoint (Sch GHC.Types.[]) _ = True disjoint (Sch (h GHC.Types.: t)) s = ((attrNotIn h s) && (disjoint (Sch t) s)) occurs :: [AChar] -> Schema -> Bool occurs _ (Sch GHC.Types.[]) = False occurs name (Sch ((Attr name' _) GHC.Types.: attrs)) = ((name == name') || (occurs name (Sch attrs))) lookup :: [AChar] -> Schema -> U lookup _ (Sch GHC.Types.[]) = undefined lookup name (Sch ((Attr name' u) GHC.Types.: attrs)) = if (name == name') then u else lookup name (Sch attrs) type family Equals_0123456789 (a :: U) (b :: U) :: Bool where Equals_0123456789 BOOL BOOL = TrueSym0 Equals_0123456789 STRING STRING = TrueSym0 Equals_0123456789 NAT NAT = TrueSym0 Equals_0123456789 (VEC a a) (VEC b b) = (:&&) ((:==) a b) ((:==) a b) Equals_0123456789 (a :: U) (b :: U) = FalseSym0 instance PEq (KProxy :: KProxy U) where type (:==) (a :: U) (b :: U) = Equals_0123456789 a b type BOOLSym0 = BOOL type STRINGSym0 = STRING type NATSym0 = NAT type VECSym2 (t :: U) (t :: Nat) = VEC t t instance SuppressUnusedWarnings VECSym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) VECSym1KindInference GHC.Tuple.()) data VECSym1 (l :: U) (l :: TyFun Nat U) = forall arg. KindOf (Apply (VECSym1 l) arg) ~ KindOf (VECSym2 l arg) => VECSym1KindInference type instance Apply (VECSym1 l) l = VECSym2 l l instance SuppressUnusedWarnings VECSym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) VECSym0KindInference GHC.Tuple.()) data VECSym0 (l :: TyFun U (TyFun Nat U -> *)) = forall arg. KindOf (Apply VECSym0 arg) ~ KindOf (VECSym1 arg) => VECSym0KindInference type instance Apply VECSym0 l = VECSym1 l type family Equals_0123456789 (a :: AChar) (b :: AChar) :: Bool where Equals_0123456789 CA CA = TrueSym0 Equals_0123456789 CB CB = TrueSym0 Equals_0123456789 CC CC = TrueSym0 Equals_0123456789 CD CD = TrueSym0 Equals_0123456789 CE CE = TrueSym0 Equals_0123456789 CF CF = TrueSym0 Equals_0123456789 CG CG = TrueSym0 Equals_0123456789 CH CH = TrueSym0 Equals_0123456789 CI CI = TrueSym0 Equals_0123456789 CJ CJ = TrueSym0 Equals_0123456789 CK CK = TrueSym0 Equals_0123456789 CL CL = TrueSym0 Equals_0123456789 CM CM = TrueSym0 Equals_0123456789 CN CN = TrueSym0 Equals_0123456789 CO CO = TrueSym0 Equals_0123456789 CP CP = TrueSym0 Equals_0123456789 CQ CQ = TrueSym0 Equals_0123456789 CR CR = TrueSym0 Equals_0123456789 CS CS = TrueSym0 Equals_0123456789 CT CT = TrueSym0 Equals_0123456789 CU CU = TrueSym0 Equals_0123456789 CV CV = TrueSym0 Equals_0123456789 CW CW = TrueSym0 Equals_0123456789 CX CX = TrueSym0 Equals_0123456789 CY CY = TrueSym0 Equals_0123456789 CZ CZ = TrueSym0 Equals_0123456789 (a :: AChar) (b :: AChar) = FalseSym0 instance PEq (KProxy :: KProxy AChar) where type (:==) (a :: AChar) (b :: AChar) = Equals_0123456789 a b type CASym0 = CA type CBSym0 = CB type CCSym0 = CC type CDSym0 = CD type CESym0 = CE type CFSym0 = CF type CGSym0 = CG type CHSym0 = CH type CISym0 = CI type CJSym0 = CJ type CKSym0 = CK type CLSym0 = CL type CMSym0 = CM type CNSym0 = CN type COSym0 = CO type CPSym0 = CP type CQSym0 = CQ type CRSym0 = CR type CSSym0 = CS type CTSym0 = CT type CUSym0 = CU type CVSym0 = CV type CWSym0 = CW type CXSym0 = CX type CYSym0 = CY type CZSym0 = CZ type AttrSym2 (t :: [AChar]) (t :: U) = Attr t t instance SuppressUnusedWarnings AttrSym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) AttrSym1KindInference GHC.Tuple.()) data AttrSym1 (l :: [AChar]) (l :: TyFun U Attribute) = forall arg. KindOf (Apply (AttrSym1 l) arg) ~ KindOf (AttrSym2 l arg) => AttrSym1KindInference type instance Apply (AttrSym1 l) l = AttrSym2 l l instance SuppressUnusedWarnings AttrSym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) AttrSym0KindInference GHC.Tuple.()) data AttrSym0 (l :: TyFun [AChar] (TyFun U Attribute -> *)) = forall arg. KindOf (Apply AttrSym0 arg) ~ KindOf (AttrSym1 arg) => AttrSym0KindInference type instance Apply AttrSym0 l = AttrSym1 l type SchSym1 (t :: [Attribute]) = Sch t instance SuppressUnusedWarnings SchSym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) SchSym0KindInference GHC.Tuple.()) data SchSym0 (l :: TyFun [Attribute] Schema) = forall arg. KindOf (Apply SchSym0 arg) ~ KindOf (SchSym1 arg) => SchSym0KindInference type instance Apply SchSym0 l = SchSym1 l type Let_0123456789Scrutinee_0123456789Sym4 t t t t = Let_0123456789Scrutinee_0123456789 t t t t instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym3 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Let_0123456789Scrutinee_0123456789Sym3KindInference GHC.Tuple.()) data Let_0123456789Scrutinee_0123456789Sym3 l l l l = forall arg. KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym3 l l l) arg) ~ KindOf (Let_0123456789Scrutinee_0123456789Sym4 l l l arg) => Let_0123456789Scrutinee_0123456789Sym3KindInference type instance Apply (Let_0123456789Scrutinee_0123456789Sym3 l l l) l = Let_0123456789Scrutinee_0123456789Sym4 l l l l instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym2 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Let_0123456789Scrutinee_0123456789Sym2KindInference GHC.Tuple.()) data Let_0123456789Scrutinee_0123456789Sym2 l l l = forall arg. KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym2 l l) arg) ~ KindOf (Let_0123456789Scrutinee_0123456789Sym3 l l arg) => Let_0123456789Scrutinee_0123456789Sym2KindInference type instance Apply (Let_0123456789Scrutinee_0123456789Sym2 l l) l = Let_0123456789Scrutinee_0123456789Sym3 l l l instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Let_0123456789Scrutinee_0123456789Sym1KindInference GHC.Tuple.()) data Let_0123456789Scrutinee_0123456789Sym1 l l = forall arg. KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym1 l) arg) ~ KindOf (Let_0123456789Scrutinee_0123456789Sym2 l arg) => Let_0123456789Scrutinee_0123456789Sym1KindInference type instance Apply (Let_0123456789Scrutinee_0123456789Sym1 l) l = Let_0123456789Scrutinee_0123456789Sym2 l l instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Let_0123456789Scrutinee_0123456789Sym0KindInference GHC.Tuple.()) data Let_0123456789Scrutinee_0123456789Sym0 l = forall arg. KindOf (Apply Let_0123456789Scrutinee_0123456789Sym0 arg) ~ KindOf (Let_0123456789Scrutinee_0123456789Sym1 arg) => Let_0123456789Scrutinee_0123456789Sym0KindInference type instance Apply Let_0123456789Scrutinee_0123456789Sym0 l = Let_0123456789Scrutinee_0123456789Sym1 l type Let_0123456789Scrutinee_0123456789 name name' u attrs = Apply (Apply (:==$) name) name' type family Case_0123456789 name name' u attrs t where Case_0123456789 name name' u attrs True = u Case_0123456789 name name' u attrs False = Apply (Apply LookupSym0 name) (Apply SchSym0 attrs) type LookupSym2 (t :: [AChar]) (t :: Schema) = Lookup t t instance SuppressUnusedWarnings LookupSym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) LookupSym1KindInference GHC.Tuple.()) data LookupSym1 (l :: [AChar]) (l :: TyFun Schema U) = forall arg. KindOf (Apply (LookupSym1 l) arg) ~ KindOf (LookupSym2 l arg) => LookupSym1KindInference type instance Apply (LookupSym1 l) l = LookupSym2 l l instance SuppressUnusedWarnings LookupSym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) LookupSym0KindInference GHC.Tuple.()) data LookupSym0 (l :: TyFun [AChar] (TyFun Schema U -> *)) = forall arg. KindOf (Apply LookupSym0 arg) ~ KindOf (LookupSym1 arg) => LookupSym0KindInference type instance Apply LookupSym0 l = LookupSym1 l type OccursSym2 (t :: [AChar]) (t :: Schema) = Occurs t t instance SuppressUnusedWarnings OccursSym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) OccursSym1KindInference GHC.Tuple.()) data OccursSym1 (l :: [AChar]) (l :: TyFun Schema Bool) = forall arg. KindOf (Apply (OccursSym1 l) arg) ~ KindOf (OccursSym2 l arg) => OccursSym1KindInference type instance Apply (OccursSym1 l) l = OccursSym2 l l instance SuppressUnusedWarnings OccursSym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) OccursSym0KindInference GHC.Tuple.()) data OccursSym0 (l :: TyFun [AChar] (TyFun Schema Bool -> *)) = forall arg. KindOf (Apply OccursSym0 arg) ~ KindOf (OccursSym1 arg) => OccursSym0KindInference type instance Apply OccursSym0 l = OccursSym1 l type AttrNotInSym2 (t :: Attribute) (t :: Schema) = AttrNotIn t t instance SuppressUnusedWarnings AttrNotInSym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) AttrNotInSym1KindInference GHC.Tuple.()) data AttrNotInSym1 (l :: Attribute) (l :: TyFun Schema Bool) = forall arg. KindOf (Apply (AttrNotInSym1 l) arg) ~ KindOf (AttrNotInSym2 l arg) => AttrNotInSym1KindInference type instance Apply (AttrNotInSym1 l) l = AttrNotInSym2 l l instance SuppressUnusedWarnings AttrNotInSym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) AttrNotInSym0KindInference GHC.Tuple.()) data AttrNotInSym0 (l :: TyFun Attribute (TyFun Schema Bool -> *)) = forall arg. KindOf (Apply AttrNotInSym0 arg) ~ KindOf (AttrNotInSym1 arg) => AttrNotInSym0KindInference type instance Apply AttrNotInSym0 l = AttrNotInSym1 l type DisjointSym2 (t :: Schema) (t :: Schema) = Disjoint t t instance SuppressUnusedWarnings DisjointSym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) DisjointSym1KindInference GHC.Tuple.()) data DisjointSym1 (l :: Schema) (l :: TyFun Schema Bool) = forall arg. KindOf (Apply (DisjointSym1 l) arg) ~ KindOf (DisjointSym2 l arg) => DisjointSym1KindInference type instance Apply (DisjointSym1 l) l = DisjointSym2 l l instance SuppressUnusedWarnings DisjointSym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) DisjointSym0KindInference GHC.Tuple.()) data DisjointSym0 (l :: TyFun Schema (TyFun Schema Bool -> *)) = forall arg. KindOf (Apply DisjointSym0 arg) ~ KindOf (DisjointSym1 arg) => DisjointSym0KindInference type instance Apply DisjointSym0 l = DisjointSym1 l type AppendSym2 (t :: Schema) (t :: Schema) = Append t t instance SuppressUnusedWarnings AppendSym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) AppendSym1KindInference GHC.Tuple.()) data AppendSym1 (l :: Schema) (l :: TyFun Schema Schema) = forall arg. KindOf (Apply (AppendSym1 l) arg) ~ KindOf (AppendSym2 l arg) => AppendSym1KindInference type instance Apply (AppendSym1 l) l = AppendSym2 l l instance SuppressUnusedWarnings AppendSym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) AppendSym0KindInference GHC.Tuple.()) data AppendSym0 (l :: TyFun Schema (TyFun Schema Schema -> *)) = forall arg. KindOf (Apply AppendSym0 arg) ~ KindOf (AppendSym1 arg) => AppendSym0KindInference type instance Apply AppendSym0 l = AppendSym1 l type family Lookup (a :: [AChar]) (a :: Schema) :: U where Lookup z (Sch '[]) = Any Lookup name (Sch ((:) (Attr name' u) attrs)) = Case_0123456789 name name' u attrs (Let_0123456789Scrutinee_0123456789Sym4 name name' u attrs) type family Occurs (a :: [AChar]) (a :: Schema) :: Bool where Occurs z (Sch '[]) = FalseSym0 Occurs name (Sch ((:) (Attr name' z) attrs)) = Apply (Apply (:||$) (Apply (Apply (:==$) name) name')) (Apply (Apply OccursSym0 name) (Apply SchSym0 attrs)) type family AttrNotIn (a :: Attribute) (a :: Schema) :: Bool where AttrNotIn z (Sch '[]) = TrueSym0 AttrNotIn (Attr name u) (Sch ((:) (Attr name' z) t)) = Apply (Apply (:&&$) (Apply (Apply (:/=$) name) name')) (Apply (Apply AttrNotInSym0 (Apply (Apply AttrSym0 name) u)) (Apply SchSym0 t)) type family Disjoint (a :: Schema) (a :: Schema) :: Bool where Disjoint (Sch '[]) z = TrueSym0 Disjoint (Sch ((:) h t)) s = Apply (Apply (:&&$) (Apply (Apply AttrNotInSym0 h) s)) (Apply (Apply DisjointSym0 (Apply SchSym0 t)) s) type family Append (a :: Schema) (a :: Schema) :: Schema where Append (Sch s1) (Sch s2) = Apply SchSym0 (Apply (Apply (:++$) s1) s2) sLookup :: forall (t :: [AChar]) (t :: Schema). Sing t -> Sing t -> Sing (Apply (Apply LookupSym0 t) t) sOccurs :: forall (t :: [AChar]) (t :: Schema). Sing t -> Sing t -> Sing (Apply (Apply OccursSym0 t) t) sAttrNotIn :: forall (t :: Attribute) (t :: Schema). Sing t -> Sing t -> Sing (Apply (Apply AttrNotInSym0 t) t) sDisjoint :: forall (t :: Schema) (t :: Schema). Sing t -> Sing t -> Sing (Apply (Apply DisjointSym0 t) t) sAppend :: forall (t :: Schema) (t :: Schema). Sing t -> Sing t -> Sing (Apply (Apply AppendSym0 t) t) sLookup _ (SSch SNil) = let lambda :: forall wild. (t ~ wild, t ~ Apply SchSym0 '[]) => Sing (Apply (Apply LookupSym0 wild) (Apply SchSym0 '[])) lambda = undefined in lambda sLookup sName (SSch (SCons (SAttr sName' sU) sAttrs)) = let lambda :: forall name name' u attrs. (t ~ name, t ~ Apply SchSym0 (Apply (Apply (:$) (Apply (Apply AttrSym0 name') u)) attrs)) => Sing name -> Sing name' -> Sing u -> Sing attrs -> Sing (Apply (Apply LookupSym0 name) (Apply SchSym0 (Apply (Apply (:$) (Apply (Apply AttrSym0 name') u)) attrs))) lambda name name' u attrs = let sScrutinee_0123456789 :: Sing (Let_0123456789Scrutinee_0123456789Sym4 name name' u attrs) sScrutinee_0123456789 = applySing (applySing (singFun2 (Proxy :: Proxy (:==$)) (%:==)) name) name' in case sScrutinee_0123456789 of { STrue -> let lambda :: Sing (Case_0123456789 name name' u attrs TrueSym0) lambda = u in lambda SFalse -> let lambda :: Sing (Case_0123456789 name name' u attrs FalseSym0) lambda = applySing (applySing (singFun2 (Proxy :: Proxy LookupSym0) sLookup) name) (applySing (singFun1 (Proxy :: Proxy SchSym0) SSch) attrs) in lambda } in lambda sName sName' sU sAttrs sOccurs _ (SSch SNil) = let lambda :: forall wild. (t ~ wild, t ~ Apply SchSym0 '[]) => Sing (Apply (Apply OccursSym0 wild) (Apply SchSym0 '[])) lambda = SFalse in lambda sOccurs sName (SSch (SCons (SAttr sName' _) sAttrs)) = let lambda :: forall name name' attrs wild. (t ~ name, t ~ Apply SchSym0 (Apply (Apply (:$) (Apply (Apply AttrSym0 name') wild)) attrs)) => Sing name -> Sing name' -> Sing attrs -> Sing (Apply (Apply OccursSym0 name) (Apply SchSym0 (Apply (Apply (:$) (Apply (Apply AttrSym0 name') wild)) attrs))) lambda name name' attrs = applySing (applySing (singFun2 (Proxy :: Proxy (:||$)) (%:||)) (applySing (applySing (singFun2 (Proxy :: Proxy (:==$)) (%:==)) name) name')) (applySing (applySing (singFun2 (Proxy :: Proxy OccursSym0) sOccurs) name) (applySing (singFun1 (Proxy :: Proxy SchSym0) SSch) attrs)) in lambda sName sName' sAttrs sAttrNotIn _ (SSch SNil) = let lambda :: forall wild. (t ~ wild, t ~ Apply SchSym0 '[]) => Sing (Apply (Apply AttrNotInSym0 wild) (Apply SchSym0 '[])) lambda = STrue in lambda sAttrNotIn (SAttr sName sU) (SSch (SCons (SAttr sName' _) sT)) = let lambda :: forall name u name' t wild. (t ~ Apply (Apply AttrSym0 name) u, t ~ Apply SchSym0 (Apply (Apply (:$) (Apply (Apply AttrSym0 name') wild)) t)) => Sing name -> Sing u -> Sing name' -> Sing t -> Sing (Apply (Apply AttrNotInSym0 (Apply (Apply AttrSym0 name) u)) (Apply SchSym0 (Apply (Apply (:$) (Apply (Apply AttrSym0 name') wild)) t))) lambda name u name' t = applySing (applySing (singFun2 (Proxy :: Proxy (:&&$)) (%:&&)) (applySing (applySing (singFun2 (Proxy :: Proxy (:/=$)) (%:/=)) name) name')) (applySing (applySing (singFun2 (Proxy :: Proxy AttrNotInSym0) sAttrNotIn) (applySing (applySing (singFun2 (Proxy :: Proxy AttrSym0) SAttr) name) u)) (applySing (singFun1 (Proxy :: Proxy SchSym0) SSch) t)) in lambda sName sU sName' sT sDisjoint (SSch SNil) _ = let lambda :: forall wild. (t ~ Apply SchSym0 '[], t ~ wild) => Sing (Apply (Apply DisjointSym0 (Apply SchSym0 '[])) wild) lambda = STrue in lambda sDisjoint (SSch (SCons sH sT)) sS = let lambda :: forall h t s. (t ~ Apply SchSym0 (Apply (Apply (:$) h) t), t ~ s) => Sing h -> Sing t -> Sing s -> Sing (Apply (Apply DisjointSym0 (Apply SchSym0 (Apply (Apply (:$) h) t))) s) lambda h t s = applySing (applySing (singFun2 (Proxy :: Proxy (:&&$)) (%:&&)) (applySing (applySing (singFun2 (Proxy :: Proxy AttrNotInSym0) sAttrNotIn) h) s)) (applySing (applySing (singFun2 (Proxy :: Proxy DisjointSym0) sDisjoint) (applySing (singFun1 (Proxy :: Proxy SchSym0) SSch) t)) s) in lambda sH sT sS sAppend (SSch sS1) (SSch sS2) = let lambda :: forall s1 s2. (t ~ Apply SchSym0 s1, t ~ Apply SchSym0 s2) => Sing s1 -> Sing s2 -> Sing (Apply (Apply AppendSym0 (Apply SchSym0 s1)) (Apply SchSym0 s2)) lambda s1 s2 = applySing (singFun1 (Proxy :: Proxy SchSym0) SSch) (applySing (applySing (singFun2 (Proxy :: Proxy (:++$)) (%:++)) s1) s2) in lambda sS1 sS2 data instance Sing (z :: U) = z ~ BOOL => SBOOL | z ~ STRING => SSTRING | z ~ NAT => SNAT | forall (n :: U) (n :: Nat). z ~ VEC n n => SVEC (Sing n) (Sing n) type SU (z :: U) = Sing z instance SingKind (KProxy :: KProxy U) where type DemoteRep (KProxy :: KProxy U) = U fromSing SBOOL = BOOL fromSing SSTRING = STRING fromSing SNAT = NAT fromSing (SVEC b b) = VEC (fromSing b) (fromSing b) toSing BOOL = SomeSing SBOOL toSing STRING = SomeSing SSTRING toSing NAT = SomeSing SNAT toSing (VEC b b) = case GHC.Tuple.(,) (toSing b :: SomeSing (KProxy :: KProxy U)) (toSing b :: SomeSing (KProxy :: KProxy Nat)) of { GHC.Tuple.(,) (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 (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SBOOL SNAT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SBOOL (SVEC _ _) = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SSTRING SBOOL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SSTRING SSTRING = Proved Refl (%~) SSTRING SNAT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SSTRING (SVEC _ _) = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SNAT SBOOL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SNAT SSTRING = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SNAT SNAT = Proved Refl (%~) SNAT (SVEC _ _) = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) (SVEC _ _) SBOOL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) (SVEC _ _) SSTRING = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) (SVEC _ _) SNAT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) (SVEC a a) (SVEC b b) = case GHC.Tuple.(,) ((%~) a b) ((%~) a b) of { GHC.Tuple.(,) (Proved Refl) (Proved Refl) -> Proved Refl GHC.Tuple.(,) (Disproved contra) _ -> Disproved (\ refl -> case refl of { Refl -> contra Refl }) GHC.Tuple.(,) _ (Disproved contra) -> Disproved (\ refl -> case refl of { Refl -> contra Refl }) } data instance Sing (z :: AChar) = z ~ CA => SCA | z ~ CB => SCB | z ~ CC => SCC | z ~ CD => SCD | z ~ CE => SCE | z ~ CF => SCF | z ~ CG => SCG | z ~ CH => SCH | z ~ CI => SCI | z ~ CJ => SCJ | z ~ CK => SCK | z ~ CL => SCL | z ~ CM => SCM | z ~ CN => SCN | z ~ CO => SCO | z ~ CP => SCP | z ~ CQ => SCQ | z ~ CR => SCR | z ~ CS => SCS | z ~ CT => SCT | z ~ CU => SCU | z ~ CV => SCV | z ~ CW => SCW | z ~ CX => SCX | z ~ CY => SCY | z ~ CZ => SCZ type SAChar (z :: AChar) = Sing z instance SingKind (KProxy :: KProxy AChar) where type DemoteRep (KProxy :: KProxy AChar) = AChar fromSing SCA = CA fromSing SCB = CB fromSing SCC = CC fromSing SCD = CD fromSing SCE = CE fromSing SCF = CF fromSing SCG = CG fromSing SCH = CH fromSing SCI = CI fromSing SCJ = CJ fromSing SCK = CK fromSing SCL = CL fromSing SCM = CM fromSing SCN = CN fromSing SCO = CO fromSing SCP = CP fromSing SCQ = CQ fromSing SCR = CR fromSing SCS = CS fromSing SCT = CT fromSing SCU = CU fromSing SCV = CV fromSing SCW = CW fromSing SCX = CX fromSing SCY = CY fromSing SCZ = CZ toSing CA = SomeSing SCA toSing CB = SomeSing SCB toSing CC = SomeSing SCC toSing CD = SomeSing SCD toSing CE = SomeSing SCE toSing CF = SomeSing SCF toSing CG = SomeSing SCG toSing CH = SomeSing SCH toSing CI = SomeSing SCI toSing CJ = SomeSing SCJ toSing CK = SomeSing SCK toSing CL = SomeSing SCL toSing CM = SomeSing SCM toSing CN = SomeSing SCN toSing CO = SomeSing SCO toSing CP = SomeSing SCP toSing CQ = SomeSing SCQ toSing CR = SomeSing SCR toSing CS = SomeSing SCS toSing CT = SomeSing SCT toSing CU = SomeSing SCU toSing CV = SomeSing SCV toSing CW = SomeSing SCW toSing CX = SomeSing SCX toSing CY = SomeSing SCY toSing CZ = SomeSing SCZ instance SEq (KProxy :: KProxy AChar) where (%:==) SCA SCA = STrue (%:==) SCA SCB = SFalse (%:==) SCA SCC = SFalse (%:==) SCA SCD = SFalse (%:==) SCA SCE = SFalse (%:==) SCA SCF = SFalse (%:==) SCA SCG = SFalse (%:==) SCA SCH = SFalse (%:==) SCA SCI = SFalse (%:==) SCA SCJ = SFalse (%:==) SCA SCK = SFalse (%:==) SCA SCL = SFalse (%:==) SCA SCM = SFalse (%:==) SCA SCN = SFalse (%:==) SCA SCO = SFalse (%:==) SCA SCP = SFalse (%:==) SCA SCQ = SFalse (%:==) SCA SCR = SFalse (%:==) SCA SCS = SFalse (%:==) SCA SCT = SFalse (%:==) SCA SCU = SFalse (%:==) SCA SCV = SFalse (%:==) SCA SCW = SFalse (%:==) SCA SCX = SFalse (%:==) SCA SCY = SFalse (%:==) SCA SCZ = SFalse (%:==) SCB SCA = SFalse (%:==) SCB SCB = STrue (%:==) SCB SCC = SFalse (%:==) SCB SCD = SFalse (%:==) SCB SCE = SFalse (%:==) SCB SCF = SFalse (%:==) SCB SCG = SFalse (%:==) SCB SCH = SFalse (%:==) SCB SCI = SFalse (%:==) SCB SCJ = SFalse (%:==) SCB SCK = SFalse (%:==) SCB SCL = SFalse (%:==) SCB SCM = SFalse (%:==) SCB SCN = SFalse (%:==) SCB SCO = SFalse (%:==) SCB SCP = SFalse (%:==) SCB SCQ = SFalse (%:==) SCB SCR = SFalse (%:==) SCB SCS = SFalse (%:==) SCB SCT = SFalse (%:==) SCB SCU = SFalse (%:==) SCB SCV = SFalse (%:==) SCB SCW = SFalse (%:==) SCB SCX = SFalse (%:==) SCB SCY = SFalse (%:==) SCB SCZ = SFalse (%:==) SCC SCA = SFalse (%:==) SCC SCB = SFalse (%:==) SCC SCC = STrue (%:==) SCC SCD = SFalse (%:==) SCC SCE = SFalse (%:==) SCC SCF = SFalse (%:==) SCC SCG = SFalse (%:==) SCC SCH = SFalse (%:==) SCC SCI = SFalse (%:==) SCC SCJ = SFalse (%:==) SCC SCK = SFalse (%:==) SCC SCL = SFalse (%:==) SCC SCM = SFalse (%:==) SCC SCN = SFalse (%:==) SCC SCO = SFalse (%:==) SCC SCP = SFalse (%:==) SCC SCQ = SFalse (%:==) SCC SCR = SFalse (%:==) SCC SCS = SFalse (%:==) SCC SCT = SFalse (%:==) SCC SCU = SFalse (%:==) SCC SCV = SFalse (%:==) SCC SCW = SFalse (%:==) SCC SCX = SFalse (%:==) SCC SCY = SFalse (%:==) SCC SCZ = SFalse (%:==) SCD SCA = SFalse (%:==) SCD SCB = SFalse (%:==) SCD SCC = SFalse (%:==) SCD SCD = STrue (%:==) SCD SCE = SFalse (%:==) SCD SCF = SFalse (%:==) SCD SCG = SFalse (%:==) SCD SCH = SFalse (%:==) SCD SCI = SFalse (%:==) SCD SCJ = SFalse (%:==) SCD SCK = SFalse (%:==) SCD SCL = SFalse (%:==) SCD SCM = SFalse (%:==) SCD SCN = SFalse (%:==) SCD SCO = SFalse (%:==) SCD SCP = SFalse (%:==) SCD SCQ = SFalse (%:==) SCD SCR = SFalse (%:==) SCD SCS = SFalse (%:==) SCD SCT = SFalse (%:==) SCD SCU = SFalse (%:==) SCD SCV = SFalse (%:==) SCD SCW = SFalse (%:==) SCD SCX = SFalse (%:==) SCD SCY = SFalse (%:==) SCD SCZ = SFalse (%:==) SCE SCA = SFalse (%:==) SCE SCB = SFalse (%:==) SCE SCC = SFalse (%:==) SCE SCD = SFalse (%:==) SCE SCE = STrue (%:==) SCE SCF = SFalse (%:==) SCE SCG = SFalse (%:==) SCE SCH = SFalse (%:==) SCE SCI = SFalse (%:==) SCE SCJ = SFalse (%:==) SCE SCK = SFalse (%:==) SCE SCL = SFalse (%:==) SCE SCM = SFalse (%:==) SCE SCN = SFalse (%:==) SCE SCO = SFalse (%:==) SCE SCP = SFalse (%:==) SCE SCQ = SFalse (%:==) SCE SCR = SFalse (%:==) SCE SCS = SFalse (%:==) SCE SCT = SFalse (%:==) SCE SCU = SFalse (%:==) SCE SCV = SFalse (%:==) SCE SCW = SFalse (%:==) SCE SCX = SFalse (%:==) SCE SCY = SFalse (%:==) SCE SCZ = SFalse (%:==) SCF SCA = SFalse (%:==) SCF SCB = SFalse (%:==) SCF SCC = SFalse (%:==) SCF SCD = SFalse (%:==) SCF SCE = SFalse (%:==) SCF SCF = STrue (%:==) SCF SCG = SFalse (%:==) SCF SCH = SFalse (%:==) SCF SCI = SFalse (%:==) SCF SCJ = SFalse (%:==) SCF SCK = SFalse (%:==) SCF SCL = SFalse (%:==) SCF SCM = SFalse (%:==) SCF SCN = SFalse (%:==) SCF SCO = SFalse (%:==) SCF SCP = SFalse (%:==) SCF SCQ = SFalse (%:==) SCF SCR = SFalse (%:==) SCF SCS = SFalse (%:==) SCF SCT = SFalse (%:==) SCF SCU = SFalse (%:==) SCF SCV = SFalse (%:==) SCF SCW = SFalse (%:==) SCF SCX = SFalse (%:==) SCF SCY = SFalse (%:==) SCF SCZ = SFalse (%:==) SCG SCA = SFalse (%:==) SCG SCB = SFalse (%:==) SCG SCC = SFalse (%:==) SCG SCD = SFalse (%:==) SCG SCE = SFalse (%:==) SCG SCF = SFalse (%:==) SCG SCG = STrue (%:==) SCG SCH = SFalse (%:==) SCG SCI = SFalse (%:==) SCG SCJ = SFalse (%:==) SCG SCK = SFalse (%:==) SCG SCL = SFalse (%:==) SCG SCM = SFalse (%:==) SCG SCN = SFalse (%:==) SCG SCO = SFalse (%:==) SCG SCP = SFalse (%:==) SCG SCQ = SFalse (%:==) SCG SCR = SFalse (%:==) SCG SCS = SFalse (%:==) SCG SCT = SFalse (%:==) SCG SCU = SFalse (%:==) SCG SCV = SFalse (%:==) SCG SCW = SFalse (%:==) SCG SCX = SFalse (%:==) SCG SCY = SFalse (%:==) SCG SCZ = SFalse (%:==) SCH SCA = SFalse (%:==) SCH SCB = SFalse (%:==) SCH SCC = SFalse (%:==) SCH SCD = SFalse (%:==) SCH SCE = SFalse (%:==) SCH SCF = SFalse (%:==) SCH SCG = SFalse (%:==) SCH SCH = STrue (%:==) SCH SCI = SFalse (%:==) SCH SCJ = SFalse (%:==) SCH SCK = SFalse (%:==) SCH SCL = SFalse (%:==) SCH SCM = SFalse (%:==) SCH SCN = SFalse (%:==) SCH SCO = SFalse (%:==) SCH SCP = SFalse (%:==) SCH SCQ = SFalse (%:==) SCH SCR = SFalse (%:==) SCH SCS = SFalse (%:==) SCH SCT = SFalse (%:==) SCH SCU = SFalse (%:==) SCH SCV = SFalse (%:==) SCH SCW = SFalse (%:==) SCH SCX = SFalse (%:==) SCH SCY = SFalse (%:==) SCH SCZ = SFalse (%:==) SCI SCA = SFalse (%:==) SCI SCB = SFalse (%:==) SCI SCC = SFalse (%:==) SCI SCD = SFalse (%:==) SCI SCE = SFalse (%:==) SCI SCF = SFalse (%:==) SCI SCG = SFalse (%:==) SCI SCH = SFalse (%:==) SCI SCI = STrue (%:==) SCI SCJ = SFalse (%:==) SCI SCK = SFalse (%:==) SCI SCL = SFalse (%:==) SCI SCM = SFalse (%:==) SCI SCN = SFalse (%:==) SCI SCO = SFalse (%:==) SCI SCP = SFalse (%:==) SCI SCQ = SFalse (%:==) SCI SCR = SFalse (%:==) SCI SCS = SFalse (%:==) SCI SCT = SFalse (%:==) SCI SCU = SFalse (%:==) SCI SCV = SFalse (%:==) SCI SCW = SFalse (%:==) SCI SCX = SFalse (%:==) SCI SCY = SFalse (%:==) SCI SCZ = SFalse (%:==) SCJ SCA = SFalse (%:==) SCJ SCB = SFalse (%:==) SCJ SCC = SFalse (%:==) SCJ SCD = SFalse (%:==) SCJ SCE = SFalse (%:==) SCJ SCF = SFalse (%:==) SCJ SCG = SFalse (%:==) SCJ SCH = SFalse (%:==) SCJ SCI = SFalse (%:==) SCJ SCJ = STrue (%:==) SCJ SCK = SFalse (%:==) SCJ SCL = SFalse (%:==) SCJ SCM = SFalse (%:==) SCJ SCN = SFalse (%:==) SCJ SCO = SFalse (%:==) SCJ SCP = SFalse (%:==) SCJ SCQ = SFalse (%:==) SCJ SCR = SFalse (%:==) SCJ SCS = SFalse (%:==) SCJ SCT = SFalse (%:==) SCJ SCU = SFalse (%:==) SCJ SCV = SFalse (%:==) SCJ SCW = SFalse (%:==) SCJ SCX = SFalse (%:==) SCJ SCY = SFalse (%:==) SCJ SCZ = SFalse (%:==) SCK SCA = SFalse (%:==) SCK SCB = SFalse (%:==) SCK SCC = SFalse (%:==) SCK SCD = SFalse (%:==) SCK SCE = SFalse (%:==) SCK SCF = SFalse (%:==) SCK SCG = SFalse (%:==) SCK SCH = SFalse (%:==) SCK SCI = SFalse (%:==) SCK SCJ = SFalse (%:==) SCK SCK = STrue (%:==) SCK SCL = SFalse (%:==) SCK SCM = SFalse (%:==) SCK SCN = SFalse (%:==) SCK SCO = SFalse (%:==) SCK SCP = SFalse (%:==) SCK SCQ = SFalse (%:==) SCK SCR = SFalse (%:==) SCK SCS = SFalse (%:==) SCK SCT = SFalse (%:==) SCK SCU = SFalse (%:==) SCK SCV = SFalse (%:==) SCK SCW = SFalse (%:==) SCK SCX = SFalse (%:==) SCK SCY = SFalse (%:==) SCK SCZ = SFalse (%:==) SCL SCA = SFalse (%:==) SCL SCB = SFalse (%:==) SCL SCC = SFalse (%:==) SCL SCD = SFalse (%:==) SCL SCE = SFalse (%:==) SCL SCF = SFalse (%:==) SCL SCG = SFalse (%:==) SCL SCH = SFalse (%:==) SCL SCI = SFalse (%:==) SCL SCJ = SFalse (%:==) SCL SCK = SFalse (%:==) SCL SCL = STrue (%:==) SCL SCM = SFalse (%:==) SCL SCN = SFalse (%:==) SCL SCO = SFalse (%:==) SCL SCP = SFalse (%:==) SCL SCQ = SFalse (%:==) SCL SCR = SFalse (%:==) SCL SCS = SFalse (%:==) SCL SCT = SFalse (%:==) SCL SCU = SFalse (%:==) SCL SCV = SFalse (%:==) SCL SCW = SFalse (%:==) SCL SCX = SFalse (%:==) SCL SCY = SFalse (%:==) SCL SCZ = SFalse (%:==) SCM SCA = SFalse (%:==) SCM SCB = SFalse (%:==) SCM SCC = SFalse (%:==) SCM SCD = SFalse (%:==) SCM SCE = SFalse (%:==) SCM SCF = SFalse (%:==) SCM SCG = SFalse (%:==) SCM SCH = SFalse (%:==) SCM SCI = SFalse (%:==) SCM SCJ = SFalse (%:==) SCM SCK = SFalse (%:==) SCM SCL = SFalse (%:==) SCM SCM = STrue (%:==) SCM SCN = SFalse (%:==) SCM SCO = SFalse (%:==) SCM SCP = SFalse (%:==) SCM SCQ = SFalse (%:==) SCM SCR = SFalse (%:==) SCM SCS = SFalse (%:==) SCM SCT = SFalse (%:==) SCM SCU = SFalse (%:==) SCM SCV = SFalse (%:==) SCM SCW = SFalse (%:==) SCM SCX = SFalse (%:==) SCM SCY = SFalse (%:==) SCM SCZ = SFalse (%:==) SCN SCA = SFalse (%:==) SCN SCB = SFalse (%:==) SCN SCC = SFalse (%:==) SCN SCD = SFalse (%:==) SCN SCE = SFalse (%:==) SCN SCF = SFalse (%:==) SCN SCG = SFalse (%:==) SCN SCH = SFalse (%:==) SCN SCI = SFalse (%:==) SCN SCJ = SFalse (%:==) SCN SCK = SFalse (%:==) SCN SCL = SFalse (%:==) SCN SCM = SFalse (%:==) SCN SCN = STrue (%:==) SCN SCO = SFalse (%:==) SCN SCP = SFalse (%:==) SCN SCQ = SFalse (%:==) SCN SCR = SFalse (%:==) SCN SCS = SFalse (%:==) SCN SCT = SFalse (%:==) SCN SCU = SFalse (%:==) SCN SCV = SFalse (%:==) SCN SCW = SFalse (%:==) SCN SCX = SFalse (%:==) SCN SCY = SFalse (%:==) SCN SCZ = SFalse (%:==) SCO SCA = SFalse (%:==) SCO SCB = SFalse (%:==) SCO SCC = SFalse (%:==) SCO SCD = SFalse (%:==) SCO SCE = SFalse (%:==) SCO SCF = SFalse (%:==) SCO SCG = SFalse (%:==) SCO SCH = SFalse (%:==) SCO SCI = SFalse (%:==) SCO SCJ = SFalse (%:==) SCO SCK = SFalse (%:==) SCO SCL = SFalse (%:==) SCO SCM = SFalse (%:==) SCO SCN = SFalse (%:==) SCO SCO = STrue (%:==) SCO SCP = SFalse (%:==) SCO SCQ = SFalse (%:==) SCO SCR = SFalse (%:==) SCO SCS = SFalse (%:==) SCO SCT = SFalse (%:==) SCO SCU = SFalse (%:==) SCO SCV = SFalse (%:==) SCO SCW = SFalse (%:==) SCO SCX = SFalse (%:==) SCO SCY = SFalse (%:==) SCO SCZ = SFalse (%:==) SCP SCA = SFalse (%:==) SCP SCB = SFalse (%:==) SCP SCC = SFalse (%:==) SCP SCD = SFalse (%:==) SCP SCE = SFalse (%:==) SCP SCF = SFalse (%:==) SCP SCG = SFalse (%:==) SCP SCH = SFalse (%:==) SCP SCI = SFalse (%:==) SCP SCJ = SFalse (%:==) SCP SCK = SFalse (%:==) SCP SCL = SFalse (%:==) SCP SCM = SFalse (%:==) SCP SCN = SFalse (%:==) SCP SCO = SFalse (%:==) SCP SCP = STrue (%:==) SCP SCQ = SFalse (%:==) SCP SCR = SFalse (%:==) SCP SCS = SFalse (%:==) SCP SCT = SFalse (%:==) SCP SCU = SFalse (%:==) SCP SCV = SFalse (%:==) SCP SCW = SFalse (%:==) SCP SCX = SFalse (%:==) SCP SCY = SFalse (%:==) SCP SCZ = SFalse (%:==) SCQ SCA = SFalse (%:==) SCQ SCB = SFalse (%:==) SCQ SCC = SFalse (%:==) SCQ SCD = SFalse (%:==) SCQ SCE = SFalse (%:==) SCQ SCF = SFalse (%:==) SCQ SCG = SFalse (%:==) SCQ SCH = SFalse (%:==) SCQ SCI = SFalse (%:==) SCQ SCJ = SFalse (%:==) SCQ SCK = SFalse (%:==) SCQ SCL = SFalse (%:==) SCQ SCM = SFalse (%:==) SCQ SCN = SFalse (%:==) SCQ SCO = SFalse (%:==) SCQ SCP = SFalse (%:==) SCQ SCQ = STrue (%:==) SCQ SCR = SFalse (%:==) SCQ SCS = SFalse (%:==) SCQ SCT = SFalse (%:==) SCQ SCU = SFalse (%:==) SCQ SCV = SFalse (%:==) SCQ SCW = SFalse (%:==) SCQ SCX = SFalse (%:==) SCQ SCY = SFalse (%:==) SCQ SCZ = SFalse (%:==) SCR SCA = SFalse (%:==) SCR SCB = SFalse (%:==) SCR SCC = SFalse (%:==) SCR SCD = SFalse (%:==) SCR SCE = SFalse (%:==) SCR SCF = SFalse (%:==) SCR SCG = SFalse (%:==) SCR SCH = SFalse (%:==) SCR SCI = SFalse (%:==) SCR SCJ = SFalse (%:==) SCR SCK = SFalse (%:==) SCR SCL = SFalse (%:==) SCR SCM = SFalse (%:==) SCR SCN = SFalse (%:==) SCR SCO = SFalse (%:==) SCR SCP = SFalse (%:==) SCR SCQ = SFalse (%:==) SCR SCR = STrue (%:==) SCR SCS = SFalse (%:==) SCR SCT = SFalse (%:==) SCR SCU = SFalse (%:==) SCR SCV = SFalse (%:==) SCR SCW = SFalse (%:==) SCR SCX = SFalse (%:==) SCR SCY = SFalse (%:==) SCR SCZ = SFalse (%:==) SCS SCA = SFalse (%:==) SCS SCB = SFalse (%:==) SCS SCC = SFalse (%:==) SCS SCD = SFalse (%:==) SCS SCE = SFalse (%:==) SCS SCF = SFalse (%:==) SCS SCG = SFalse (%:==) SCS SCH = SFalse (%:==) SCS SCI = SFalse (%:==) SCS SCJ = SFalse (%:==) SCS SCK = SFalse (%:==) SCS SCL = SFalse (%:==) SCS SCM = SFalse (%:==) SCS SCN = SFalse (%:==) SCS SCO = SFalse (%:==) SCS SCP = SFalse (%:==) SCS SCQ = SFalse (%:==) SCS SCR = SFalse (%:==) SCS SCS = STrue (%:==) SCS SCT = SFalse (%:==) SCS SCU = SFalse (%:==) SCS SCV = SFalse (%:==) SCS SCW = SFalse (%:==) SCS SCX = SFalse (%:==) SCS SCY = SFalse (%:==) SCS SCZ = SFalse (%:==) SCT SCA = SFalse (%:==) SCT SCB = SFalse (%:==) SCT SCC = SFalse (%:==) SCT SCD = SFalse (%:==) SCT SCE = SFalse (%:==) SCT SCF = SFalse (%:==) SCT SCG = SFalse (%:==) SCT SCH = SFalse (%:==) SCT SCI = SFalse (%:==) SCT SCJ = SFalse (%:==) SCT SCK = SFalse (%:==) SCT SCL = SFalse (%:==) SCT SCM = SFalse (%:==) SCT SCN = SFalse (%:==) SCT SCO = SFalse (%:==) SCT SCP = SFalse (%:==) SCT SCQ = SFalse (%:==) SCT SCR = SFalse (%:==) SCT SCS = SFalse (%:==) SCT SCT = STrue (%:==) SCT SCU = SFalse (%:==) SCT SCV = SFalse (%:==) SCT SCW = SFalse (%:==) SCT SCX = SFalse (%:==) SCT SCY = SFalse (%:==) SCT SCZ = SFalse (%:==) SCU SCA = SFalse (%:==) SCU SCB = SFalse (%:==) SCU SCC = SFalse (%:==) SCU SCD = SFalse (%:==) SCU SCE = SFalse (%:==) SCU SCF = SFalse (%:==) SCU SCG = SFalse (%:==) SCU SCH = SFalse (%:==) SCU SCI = SFalse (%:==) SCU SCJ = SFalse (%:==) SCU SCK = SFalse (%:==) SCU SCL = SFalse (%:==) SCU SCM = SFalse (%:==) SCU SCN = SFalse (%:==) SCU SCO = SFalse (%:==) SCU SCP = SFalse (%:==) SCU SCQ = SFalse (%:==) SCU SCR = SFalse (%:==) SCU SCS = SFalse (%:==) SCU SCT = SFalse (%:==) SCU SCU = STrue (%:==) SCU SCV = SFalse (%:==) SCU SCW = SFalse (%:==) SCU SCX = SFalse (%:==) SCU SCY = SFalse (%:==) SCU SCZ = SFalse (%:==) SCV SCA = SFalse (%:==) SCV SCB = SFalse (%:==) SCV SCC = SFalse (%:==) SCV SCD = SFalse (%:==) SCV SCE = SFalse (%:==) SCV SCF = SFalse (%:==) SCV SCG = SFalse (%:==) SCV SCH = SFalse (%:==) SCV SCI = SFalse (%:==) SCV SCJ = SFalse (%:==) SCV SCK = SFalse (%:==) SCV SCL = SFalse (%:==) SCV SCM = SFalse (%:==) SCV SCN = SFalse (%:==) SCV SCO = SFalse (%:==) SCV SCP = SFalse (%:==) SCV SCQ = SFalse (%:==) SCV SCR = SFalse (%:==) SCV SCS = SFalse (%:==) SCV SCT = SFalse (%:==) SCV SCU = SFalse (%:==) SCV SCV = STrue (%:==) SCV SCW = SFalse (%:==) SCV SCX = SFalse (%:==) SCV SCY = SFalse (%:==) SCV SCZ = SFalse (%:==) SCW SCA = SFalse (%:==) SCW SCB = SFalse (%:==) SCW SCC = SFalse (%:==) SCW SCD = SFalse (%:==) SCW SCE = SFalse (%:==) SCW SCF = SFalse (%:==) SCW SCG = SFalse (%:==) SCW SCH = SFalse (%:==) SCW SCI = SFalse (%:==) SCW SCJ = SFalse (%:==) SCW SCK = SFalse (%:==) SCW SCL = SFalse (%:==) SCW SCM = SFalse (%:==) SCW SCN = SFalse (%:==) SCW SCO = SFalse (%:==) SCW SCP = SFalse (%:==) SCW SCQ = SFalse (%:==) SCW SCR = SFalse (%:==) SCW SCS = SFalse (%:==) SCW SCT = SFalse (%:==) SCW SCU = SFalse (%:==) SCW SCV = SFalse (%:==) SCW SCW = STrue (%:==) SCW SCX = SFalse (%:==) SCW SCY = SFalse (%:==) SCW SCZ = SFalse (%:==) SCX SCA = SFalse (%:==) SCX SCB = SFalse (%:==) SCX SCC = SFalse (%:==) SCX SCD = SFalse (%:==) SCX SCE = SFalse (%:==) SCX SCF = SFalse (%:==) SCX SCG = SFalse (%:==) SCX SCH = SFalse (%:==) SCX SCI = SFalse (%:==) SCX SCJ = SFalse (%:==) SCX SCK = SFalse (%:==) SCX SCL = SFalse (%:==) SCX SCM = SFalse (%:==) SCX SCN = SFalse (%:==) SCX SCO = SFalse (%:==) SCX SCP = SFalse (%:==) SCX SCQ = SFalse (%:==) SCX SCR = SFalse (%:==) SCX SCS = SFalse (%:==) SCX SCT = SFalse (%:==) SCX SCU = SFalse (%:==) SCX SCV = SFalse (%:==) SCX SCW = SFalse (%:==) SCX SCX = STrue (%:==) SCX SCY = SFalse (%:==) SCX SCZ = SFalse (%:==) SCY SCA = SFalse (%:==) SCY SCB = SFalse (%:==) SCY SCC = SFalse (%:==) SCY SCD = SFalse (%:==) SCY SCE = SFalse (%:==) SCY SCF = SFalse (%:==) SCY SCG = SFalse (%:==) SCY SCH = SFalse (%:==) SCY SCI = SFalse (%:==) SCY SCJ = SFalse (%:==) SCY SCK = SFalse (%:==) SCY SCL = SFalse (%:==) SCY SCM = SFalse (%:==) SCY SCN = SFalse (%:==) SCY SCO = SFalse (%:==) SCY SCP = SFalse (%:==) SCY SCQ = SFalse (%:==) SCY SCR = SFalse (%:==) SCY SCS = SFalse (%:==) SCY SCT = SFalse (%:==) SCY SCU = SFalse (%:==) SCY SCV = SFalse (%:==) SCY SCW = SFalse (%:==) SCY SCX = SFalse (%:==) SCY SCY = STrue (%:==) SCY SCZ = SFalse (%:==) SCZ SCA = SFalse (%:==) SCZ SCB = SFalse (%:==) SCZ SCC = SFalse (%:==) SCZ SCD = SFalse (%:==) SCZ SCE = SFalse (%:==) SCZ SCF = SFalse (%:==) SCZ SCG = SFalse (%:==) SCZ SCH = SFalse (%:==) SCZ SCI = SFalse (%:==) SCZ SCJ = SFalse (%:==) SCZ SCK = SFalse (%:==) SCZ SCL = SFalse (%:==) SCZ SCM = SFalse (%:==) SCZ SCN = SFalse (%:==) SCZ SCO = SFalse (%:==) SCZ SCP = SFalse (%:==) SCZ SCQ = SFalse (%:==) SCZ SCR = SFalse (%:==) SCZ SCS = SFalse (%:==) SCZ SCT = SFalse (%:==) SCZ SCU = SFalse (%:==) SCZ SCV = SFalse (%:==) SCZ SCW = SFalse (%:==) SCZ SCX = SFalse (%:==) SCZ SCY = SFalse (%:==) SCZ SCZ = STrue instance SDecide (KProxy :: KProxy AChar) where (%~) SCA SCA = Proved Refl (%~) SCA SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCA SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCB = Proved Refl (%~) SCB SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCB SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCC = Proved Refl (%~) SCC SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCC SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCD = Proved Refl (%~) SCD SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCD SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCE = Proved Refl (%~) SCE SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCE SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCF = Proved Refl (%~) SCF SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCF SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCG = Proved Refl (%~) SCG SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCG SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCH = Proved Refl (%~) SCH SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCH SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCI = Proved Refl (%~) SCI SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCI SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCJ = Proved Refl (%~) SCJ SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCJ SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCK = Proved Refl (%~) SCK SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCK SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCL = Proved Refl (%~) SCL SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCL SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCM = Proved Refl (%~) SCM SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCM SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCN = Proved Refl (%~) SCN SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCN SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCO = Proved Refl (%~) SCO SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCO SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCP = Proved Refl (%~) SCP SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCP SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCQ = Proved Refl (%~) SCQ SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCQ SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCR = Proved Refl (%~) SCR SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCR SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCS = Proved Refl (%~) SCS SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCS SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCT = Proved Refl (%~) SCT SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCT SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCU = Proved Refl (%~) SCU SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCU SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCV = Proved Refl (%~) SCV SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCV SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCW = Proved Refl (%~) SCW SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCW SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCX = Proved Refl (%~) SCX SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCX SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCY SCY = Proved Refl (%~) SCY SCZ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCA = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCB = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCC = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCD = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCE = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCF = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCG = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCH = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCI = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCJ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCK = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCL = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCM = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCN = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCO = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCP = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCQ = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCR = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCS = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCT = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCU = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCV = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCW = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCX = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCY = Disproved (\ x -> case x of { _ -> error "Empty case reached -- this should be impossible" }) (%~) SCZ SCZ = Proved Refl data instance Sing (z :: Attribute) = forall (n :: [AChar]) (n :: U). z ~ Attr n n => SAttr (Sing n) (Sing n) type SAttribute (z :: Attribute) = Sing z instance SingKind (KProxy :: KProxy Attribute) where type DemoteRep (KProxy :: KProxy Attribute) = Attribute fromSing (SAttr b b) = Attr (fromSing b) (fromSing b) toSing (Attr b b) = case GHC.Tuple.(,) (toSing b :: SomeSing (KProxy :: KProxy [AChar])) (toSing b :: SomeSing (KProxy :: KProxy U)) of { GHC.Tuple.(,) (SomeSing c) (SomeSing c) -> SomeSing (SAttr c c) } data instance Sing (z :: Schema) = forall (n :: [Attribute]). z ~ Sch n => SSch (Sing n) type SSchema (z :: Schema) = Sing z instance SingKind (KProxy :: KProxy Schema) where type DemoteRep (KProxy :: KProxy Schema) = Schema fromSing (SSch b) = Sch (fromSing b) toSing (Sch b) = case toSing b :: SomeSing (KProxy :: KProxy [Attribute]) of { SomeSing c -> SomeSing (SSch c) } instance SingI BOOL where sing = SBOOL instance SingI STRING where sing = SSTRING instance SingI NAT where sing = SNAT instance (SingI n, SingI n) => SingI (VEC (n :: U) (n :: Nat)) where sing = SVEC sing sing instance SingI CA where sing = SCA instance SingI CB where sing = SCB instance SingI CC where sing = SCC instance SingI CD where sing = SCD instance SingI CE where sing = SCE instance SingI CF where sing = SCF instance SingI CG where sing = SCG instance SingI CH where sing = SCH instance SingI CI where sing = SCI instance SingI CJ where sing = SCJ instance SingI CK where sing = SCK instance SingI CL where sing = SCL instance SingI CM where sing = SCM instance SingI CN where sing = SCN instance SingI CO where sing = SCO instance SingI CP where sing = SCP instance SingI CQ where sing = SCQ instance SingI CR where sing = SCR instance SingI CS where sing = SCS instance SingI CT where sing = SCT instance SingI CU where sing = SCU instance SingI CV where sing = SCV instance SingI CW where sing = SCW instance SingI CX where sing = SCX instance SingI CY where sing = SCY instance SingI CZ where sing = SCZ instance (SingI n, SingI n) => SingI (Attr (n :: [AChar]) (n :: U)) where sing = SAttr sing sing instance SingI n => SingI (Sch (n :: [Attribute])) where sing = SSch sing GradingClient/Database.hs:0:0: Splicing declarations return [] ======> GradingClient/Database.hs:0:0: 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 }