diff --git a/Language/Symantic/Compiling/Test.hs b/Language/Symantic/Compiling/Test.hs
--- a/Language/Symantic/Compiling/Test.hs
+++ b/Language/Symantic/Compiling/Test.hs
@@ -27,13 +27,13 @@
 
 test_parseTerm ::
  forall ss src.
- Inj_Modules src ss =>
- Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity)) =>
+ ModulesInj src ss =>
+ Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports NameTe, Modules src ss) Identity)) =>
  Text ->
  Either (P.ParseError Char P.Dec) (AST_Term src ss)
 test_parseTerm inp =
-	let mods :: Modules src ss = either (error . show) id inj_Modules in
-	let imps = importQualifiedAs [] mods in
+	let mods :: Modules src ss = either (error . show) id modulesInj in
+	let imps = [] `importModules` mods in
 	runIdentity $
 	MC.evalStateStrict (imps, mods) $
 	P.runParserT g "" inp
@@ -42,19 +42,20 @@
 test_readTerm ::
  forall src ss t.
  ( Eq t
- , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity))
+ , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports NameTe, Modules src ss) Identity))
  , Show t
  , Syms ss Eval
  , Syms ss View
  , Syms ss (BetaT View)
- , Inj_Modules src ss
+ , ModulesInj src ss
  , Eq src
  , Show src
- , Inj_Source (TypeVT src) src
- , Inj_Source (TypeT src '[]) src
- , Inj_Source (KindK src) src
- , Inj_Source (AST_Type src) src
- , Inj_Name2Type ss
+ , SourceInj (TypeVT src) src
+ , SourceInj (TypeT src '[]) src
+ , SourceInj (KindK src) src
+ , SourceInj (AST_Type src) src
+ , ModulesTyInj ss
+ , ImportTypes ss
  ) =>
  Text ->
  Either ( Type src '[] t
@@ -67,8 +68,9 @@
 	case reduceTeApp <$> test_parseTerm @ss inp of
 	 Left err -> Left (Left err) @?= snd `left` expected
 	 Right ast ->
-		let tys = inj_Name2Type @ss in
-		case readTerm tys CtxTyZ ast of
+		let modsTy = modulesTyInj @ss in
+		let imps = importTypes @ss [] in
+		case readTerm imps modsTy CtxTyZ ast of
 		 Left err -> Left (Right err) @?= snd `left` expected
 		 Right term ->
 			case term of
diff --git a/Language/Symantic/Grammar/Megaparsec.hs b/Language/Symantic/Grammar/Megaparsec.hs
--- a/Language/Symantic/Grammar/Megaparsec.hs
+++ b/Language/Symantic/Grammar/Megaparsec.hs
@@ -23,6 +23,7 @@
 
 import Language.Symantic.Grammar as Sym
 import qualified Language.Symantic as Sym
+import Language.Symantic.Lib ()
 
 --
 -- Readers
@@ -30,10 +31,10 @@
 
 -- NonEmpty P.SourcePos
 instance ParsecC e s => Sym.Gram_Reader (NonEmpty P.SourcePos) (P.ParsecT e s m) where
-	g_ask_before g = do
+	askBefore g = do
 		s <- P.statePos <$> P.getParserState
 		($ s) <$> g
-	g_ask_after g = do
+	askAfter g = do
 		f <- g
 		f . P.statePos <$> P.getParserState
 type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader (NonEmpty P.SourcePos)) = 'True
@@ -41,10 +42,10 @@
 	askN _n = P.statePos <$> P.getParserState
 -- P.SourcePos
 instance ParsecC e s => Sym.Gram_Reader P.SourcePos (P.ParsecT e s m) where
-	g_ask_before g = do
+	askBefore g = do
 		s <- P.getPosition
 		($ s) <$> g
-	g_ask_after g = do
+	askAfter g = do
 		f <- g
 		f <$> P.getPosition
 type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader P.SourcePos) = 'True
@@ -52,8 +53,8 @@
 	askN _n = P.getPosition
 -- ()
 instance ParsecC e s => Sym.Gram_Reader () (P.ParsecT e s m) where
-	g_ask_before = fmap ($ ())
-	g_ask_after  = fmap ($ ())
+	askBefore = fmap ($ ())
+	askAfter  = fmap ($ ())
 
 --
 -- States
@@ -62,27 +63,27 @@
 -- st
 type instance MC.CanDo (P.ParsecT e s m) (MC.EffState st) = 'False
 instance (Monad m, MC.MonadState st m) => Sym.Gram_State st m where
-	g_state_before g = do
+	stateBefore g = do
 		s <- MC.get
 		f <- g
 		let (s', a) = f s
 		MC.put s'
 		return a
-	g_state_after g = do
+	stateAfter g = do
 		f <- g
 		s <- MC.get
 		let (s_, a) = f s
 		MC.put s_
 		return a
-	g_get_before g = do
+	getBefore g = do
 		s <- MC.get
 		f <- g
 		return (f s)
-	g_get_after g = do
+	getAfter g = do
 		f <- g
 		s <- MC.get
 		return (f s)
-	g_put g = do
+	put g = do
 		(s, a) <- g
 		MC.put s
 		return a
@@ -97,7 +98,7 @@
 -- Sym instances
 --
 instance (ParsecC e s, Show err) => Sym.Gram_Error err (P.ParsecT e s m) where
-	g_catch me = do
+	catch me {- if you can :-} = do
 		e <- me
 		case e of
 		 Left err -> fail $ show err
@@ -137,7 +138,9 @@
 	minus (CF f) (Reg p) = CF $ P.notFollowedBy (P.try p) *> f
 instance ParsecC e s => Sym.Gram_Comment (P.ParsecT e s m)
 instance ParsecC e s => Sym.Gram_Op (P.ParsecT e s m)
-instance ParsecC e s => Sym.Gram_Name (P.ParsecT e s m)
+instance ParsecC e s => Sym.Gram_Mod (P.ParsecT e s m)
+instance ParsecC e s => Sym.Gram_Type_Name (P.ParsecT e s m)
+instance ParsecC e s => Sym.Gram_Term_Name (P.ParsecT e s m)
 instance -- Sym.Gram_Type
  ( ParsecC e s
  , Gram_Source src      (P.ParsecT e s m)
@@ -149,7 +152,8 @@
 instance -- Sym.Gram_Term
  ( ParsecC e s
  , Show src
- , MC.MonadState (Sym.Imports, Sym.Modules src ss) (P.ParsecT e s m)
- , Sym.Gram_Source src                             (P.ParsecT e s m)
- , Sym.Gram_Term_Atoms src ss                      (P.ParsecT e s m)
- ) => Sym.Gram_Term src ss                         (P.ParsecT e s m)
+ , MC.MonadState ( Sym.Imports Sym.NameTe
+                 , Sym.Modules src ss ) (P.ParsecT e s m)
+ , Sym.Gram_Source src                  (P.ParsecT e s m)
+ , Sym.Gram_Term_Atoms src ss           (P.ParsecT e s m)
+ ) => Sym.Gram_Term src ss              (P.ParsecT e s m)
diff --git a/Language/Symantic/Lib/Alternative.hs b/Language/Symantic/Lib/Alternative.hs
--- a/Language/Symantic/Lib/Alternative.hs
+++ b/Language/Symantic/Lib/Alternative.hs
@@ -12,7 +12,7 @@
 import Language.Symantic.Lib.Function (a0)
 
 -- * Class 'Sym_Alternative'
-type instance Sym (Proxy Alternative) = Sym_Alternative
+type instance Sym Alternative = Sym_Alternative
 class Sym_Functor term => Sym_Alternative term where
 	empty :: Alternative f => term (f a)
 	(<|>) :: Alternative f => term (f a) -> term (f a) -> term (f a)
@@ -39,13 +39,15 @@
 instance (Sym_Lambda term, Sym_Alternative term) => Sym_Alternative (BetaT term)
 
 -- Typing
+instance NameTyOf Alternative where
+	nameTyOf _c = ["Alternative"] `Mod` "Alternative"
 instance FixityOf Alternative
 instance ClassInstancesFor Alternative
 instance TypeInstancesFor Alternative
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Alternative
-instance (Source src, Inj_Sym ss Alternative) => ModuleFor src ss Alternative where
+instance (Source src, SymInj ss Alternative) => ModuleFor src ss Alternative where
 	moduleFor = ["Alternative"] `moduleWhere`
 	 [ "empty" := teAlternative_empty
 	 , "<|>" `withInfixL` 3 := teAlternative_alt
diff --git a/Language/Symantic/Lib/Applicative.hs b/Language/Symantic/Lib/Applicative.hs
--- a/Language/Symantic/Lib/Applicative.hs
+++ b/Language/Symantic/Lib/Applicative.hs
@@ -13,7 +13,7 @@
 import Language.Symantic.Lib.Functor (Sym_Functor(..), (<$>), f1, f2)
 
 -- * Class 'Sym_Applicative'
-type instance Sym (Proxy Applicative) = Sym_Applicative
+type instance Sym Applicative = Sym_Applicative
 class Sym_Functor term => Sym_Applicative term where
 	pure  :: Applicative f => term a -> term (f a)
 	(<*>) :: Applicative f => term (f (a -> b)) -> term (f a) -> term (f b); infixl 4 <*>
@@ -49,13 +49,15 @@
 	(*>) = trans2 (*>)
 
 -- Typing
+instance NameTyOf Applicative where
+	nameTyOf _c = ["Applicative"] `Mod` "Applicative"
 instance FixityOf Applicative
 instance ClassInstancesFor Applicative
 instance TypeInstancesFor Applicative
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Applicative
-instance (Source src, Inj_Sym ss Applicative) => ModuleFor src ss Applicative where
+instance (Source src, SymInj ss Applicative) => ModuleFor src ss Applicative where
 	moduleFor = ["Applicative"] `moduleWhere`
 	 [ "<*>" `withInfixL` 4 := teApplicative_app
 	 , "<*"  `withInfixL` 4 := teApplicative_const
diff --git a/Language/Symantic/Lib/Bool.hs b/Language/Symantic/Lib/Bool.hs
--- a/Language/Symantic/Lib/Bool.hs
+++ b/Language/Symantic/Lib/Bool.hs
@@ -4,7 +4,6 @@
 module Language.Symantic.Lib.Bool where
 
 import Control.Monad
-import Data.Proxy
 import Prelude hiding ((&&), not, (||))
 import qualified Data.Bool as Bool
 import qualified Data.Text as Text
@@ -13,7 +12,7 @@
 import Language.Symantic.Lib.Function ()
 
 -- * Class 'Sym_Bool'
-type instance Sym (Proxy Bool) = Sym_Bool
+type instance Sym Bool = Sym_Bool
 class Sym_Bool term where
 	bool ::      Bool -> term Bool
 	not  :: term Bool -> term Bool
@@ -56,6 +55,8 @@
 	xor = trans2 xor
 
 -- Typing
+instance NameTyOf Bool where
+	nameTyOf _c = ["Bool"] `Mod` "Bool"
 instance ClassInstancesFor Bool where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
 	 | Just HRefl <- proj_ConstKiTy @_ @Bool c
@@ -71,7 +72,7 @@
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Bool
-instance (Source src, Inj_Sym ss Bool) => ModuleFor src ss Bool where
+instance (Source src, SymInj ss Bool) => ModuleFor src ss Bool where
 	moduleFor = ["Bool"] `moduleWhere`
 	 [ "False" := teBool False
 	 , "True"  := teBool True
@@ -82,11 +83,11 @@
 	 ]
 
 -- ** 'Type's
-tyBool :: Source src => Inj_Len vs => Type src vs Bool
+tyBool :: Source src => LenInj vs => Type src vs Bool
 tyBool = tyConst @(K Bool) @Bool
 
 -- ** 'Term's
-teBool :: Source src => Inj_Sym ss Bool => Bool -> Term src ss ts '[] (() #> Bool)
+teBool :: Source src => SymInj ss Bool => Bool -> Term src ss ts '[] (() #> Bool)
 teBool b = Term noConstraint tyBool $ teSym @Bool $ bool b
 
 teBool_not :: TermDef Bool '[] (() #> (Bool -> Bool))
diff --git a/Language/Symantic/Lib/Bounded.hs b/Language/Symantic/Lib/Bounded.hs
--- a/Language/Symantic/Lib/Bounded.hs
+++ b/Language/Symantic/Lib/Bounded.hs
@@ -11,7 +11,7 @@
 import Language.Symantic.Lib.Function (a0)
 
 -- * Class 'Sym_Bounded'
-type instance Sym (Proxy Bounded) = Sym_Bounded
+type instance Sym Bounded = Sym_Bounded
 class Sym_Bounded term where
 	minBound :: Bounded a => term a
 	maxBound :: Bounded a => term a
@@ -35,13 +35,15 @@
 instance (Sym_Lambda term, Sym_Bounded term) => Sym_Bounded (BetaT term)
 
 -- Typing
+instance NameTyOf Bounded where
+	nameTyOf _c = ["Bounded"] `Mod` "Bounded"
 instance FixityOf Bounded
 instance ClassInstancesFor Bounded
 instance TypeInstancesFor Bounded
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Bounded
-instance (Source src, Inj_Sym ss Bounded) => ModuleFor src ss Bounded where
+instance (Source src, SymInj ss Bounded) => ModuleFor src ss Bounded where
 	moduleFor = ["Bounded"] `moduleWhere`
 	 [ "minBound" := teBounded_minBound
 	 , "maxBound" := teBounded_maxBound
diff --git a/Language/Symantic/Lib/Char.hs b/Language/Symantic/Lib/Char.hs
--- a/Language/Symantic/Lib/Char.hs
+++ b/Language/Symantic/Lib/Char.hs
@@ -7,12 +7,12 @@
 import qualified Data.Text as Text
 
 import Language.Symantic.Grammar hiding (char, any)
-import qualified Language.Symantic.Grammar as Gram
+import qualified Language.Symantic.Grammar as G
 import Language.Symantic
 import Language.Symantic.Lib.List (tyList)
 
 -- * Class 'Sym_Char'
-type instance Sym (Proxy Char) = Sym_Char
+type instance Sym Char = Sym_Char
 class Sym_Char term where
 	char :: Char -> term Char
 	char_toUpper :: term Char -> term Char
@@ -45,6 +45,8 @@
 instance (Sym_Char term, Sym_Lambda term) => Sym_Char (BetaT term)
 
 -- Typing
+instance NameTyOf Char where
+	nameTyOf _c = ["Char"] `Mod` "Char"
 instance ClassInstancesFor Char where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
 	 | Just HRefl <- proj_ConstKiTy @_ @Char z
@@ -64,35 +66,35 @@
  , Gram_Alt g
  , Gram_Rule g
  , Gram_Comment g
- , Inj_Sym ss Char
+ , SymInj ss Char
  ) => Gram_Term_AtomsFor src ss g Char where
 	g_term_atomsFor =
 	 [ rule "teChar" $
-		lexeme $ g_source $
+		lexeme $ source $
 		(\c src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teChar c)
 		 <$> between tickG tickG (
-			cf_of_Terminal (Gram.any `but` tickG) <+>
+			cfOf (G.any `but` tickG) <+>
 			'\'' <$ string "\\'"
 		 )
 	 ]
 		where
 		tickG :: Gram_Terminal g' => g' Char
-		tickG = Gram.char '\''
-instance (Source src, Inj_Sym ss Char) => ModuleFor src ss Char where
+		tickG = G.char '\''
+instance (Source src, SymInj ss Char) => ModuleFor src ss Char where
 	moduleFor = ["Char"] `moduleWhere`
 	 [ "toLower" := teChar_toLower
 	 , "toUpper" := teChar_toUpper
 	 ]
 
 -- ** 'Type's
-tyChar :: Source src => Inj_Len vs => Type src vs Char
+tyChar :: Source src => LenInj vs => Type src vs Char
 tyChar = tyConst @(K Char) @Char
 
-tyString :: Source src => Inj_Len vs => Type src vs String
+tyString :: Source src => LenInj vs => Type src vs String
 tyString = tyList tyChar
 
 -- ** 'Term's
-teChar :: Source src => Inj_Sym ss Char => Char -> Term src ss ts '[] (() #> Char)
+teChar :: Source src => SymInj ss Char => Char -> Term src ss ts '[] (() #> Char)
 teChar b = Term noConstraint tyChar $ teSym @Char $ char b
 
 teChar_toUpper, teChar_toLower :: TermDef Char '[] (() #> (Char -> Char))
diff --git a/Language/Symantic/Lib/Either.hs b/Language/Symantic/Lib/Either.hs
--- a/Language/Symantic/Lib/Either.hs
+++ b/Language/Symantic/Lib/Either.hs
@@ -12,7 +12,7 @@
 import Language.Symantic.Lib.Function (a0, b1, c2)
 
 -- * Class 'Sym_Either'
-type instance Sym (Proxy Either) = Sym_Either
+type instance Sym Either = Sym_Either
 class Sym_Either term where
 	_Left  :: term l -> term (Either l r)
 	_Right :: term r -> term (Either l r)
@@ -44,6 +44,8 @@
 instance (Sym_Either term, Sym_Lambda term) => Sym_Either (BetaT term)
 
 -- Typing
+instance NameTyOf Either where
+	nameTyOf _c = ["Either"] `Mod` "Either"
 instance FixityOf Either
 instance ClassInstancesFor Either where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _l))
@@ -80,7 +82,7 @@
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Either
-instance (Source src, Inj_Sym ss Either) => ModuleFor src ss Either where
+instance (Source src, SymInj ss Either) => ModuleFor src ss Either where
 	moduleFor = ["Either"] `moduleWhere`
 	 [ "Left"   := teEither_Left
 	 , "Right"  := teEither_Right
diff --git a/Language/Symantic/Lib/Enum.hs b/Language/Symantic/Lib/Enum.hs
--- a/Language/Symantic/Lib/Enum.hs
+++ b/Language/Symantic/Lib/Enum.hs
@@ -12,7 +12,7 @@
 import Language.Symantic.Lib.Int (tyInt)
 
 -- * Class 'Sym_Enum'
-type instance Sym (Proxy Enum) = Sym_Enum
+type instance Sym Enum = Sym_Enum
 class Sym_Enum term where
 	toEnum   :: Enum a => term Int -> term a
 	fromEnum :: Enum a => term a -> term Int
@@ -50,13 +50,15 @@
 instance (Sym_Enum term, Sym_Lambda term) => Sym_Enum (BetaT term)
 
 -- Typing
+instance NameTyOf Enum where
+	nameTyOf _c = ["Enum"] `Mod` "Enum"
 instance FixityOf Enum
 instance ClassInstancesFor Enum
 instance TypeInstancesFor Enum
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Enum
-instance (Source src, Inj_Sym ss Enum) => ModuleFor src ss Enum where
+instance (Source src, SymInj ss Enum) => ModuleFor src ss Enum where
 	moduleFor = ["Enum"] `moduleWhere`
 	 [ "succ"     := teEnum_succ
 	 , "pred"     := teEnum_pred
diff --git a/Language/Symantic/Lib/Eq.hs b/Language/Symantic/Lib/Eq.hs
--- a/Language/Symantic/Lib/Eq.hs
+++ b/Language/Symantic/Lib/Eq.hs
@@ -11,7 +11,7 @@
 import Language.Symantic.Lib.Function (a0)
 
 -- * Class 'Sym_Eq'
-type instance Sym (Proxy Eq) = Sym_Eq
+type instance Sym Eq = Sym_Eq
 class Sym_Eq term where
 	(==) :: Eq a => term a -> term a -> term Bool; infix 4 ==
 	(/=) :: Eq a => term a -> term a -> term Bool; infix 4 /=
@@ -37,13 +37,15 @@
 instance (Sym_Eq term, Sym_Lambda term) => Sym_Eq (BetaT term)
 
 -- Typing
+instance NameTyOf Eq where
+	nameTyOf _c = ["Eq"] `Mod` "Eq"
 instance FixityOf Eq
 instance ClassInstancesFor Eq
 instance TypeInstancesFor Eq
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Eq
-instance (Source src, Inj_Sym ss Eq) => ModuleFor src ss Eq where
+instance (Source src, SymInj ss Eq) => ModuleFor src ss Eq where
 	moduleFor = ["Eq"] `moduleWhere`
 	 [ "==" `withInfixN` 4 := teEq_eq
 	 , "/=" `withInfixN` 4 := teEq_ne
diff --git a/Language/Symantic/Lib/Foldable.hs b/Language/Symantic/Lib/Foldable.hs
--- a/Language/Symantic/Lib/Foldable.hs
+++ b/Language/Symantic/Lib/Foldable.hs
@@ -25,7 +25,7 @@
 import Language.Symantic.Lib.Ord (tyOrd)
 
 -- * Class 'Sym_Foldable'
-type instance Sym (Proxy Foldable) = Sym_Foldable
+type instance Sym Foldable = Sym_Foldable
 class Sym_Foldable term where
 	foldMap    :: Foldable f => Monoid m      => term (a -> m) -> term (f a) -> term m
 	foldr      :: Foldable f                  => term (a -> b -> b) -> term b -> term (f a) -> term b
@@ -237,13 +237,15 @@
 instance (Sym_Foldable term, Sym_Lambda term) => Sym_Foldable (BetaT term)
 
 -- Typing
+instance NameTyOf Foldable where
+	nameTyOf _c = ["Foldable"] `Mod` "Foldable"
 instance FixityOf Foldable
 instance ClassInstancesFor Foldable
 instance TypeInstancesFor Foldable
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Foldable
-instance (Source src, Inj_Sym ss Foldable) => ModuleFor src ss Foldable where
+instance (Source src, SymInj ss Foldable) => ModuleFor src ss Foldable where
 	moduleFor = ["Foldable"] `moduleWhere`
 	 [ "foldMap" := teFoldable_foldMap
 	 , "foldr"   := teFoldable_foldr
@@ -266,15 +268,15 @@
 tyFoldable :: Source src => Type src vs a -> Type src vs (Foldable a)
 tyFoldable a = tyConstLen @(K Foldable) @Foldable (lenVars a) `tyApp` a
 
-t0 :: Source src => Inj_Len vs => Inj_Kind (K t) =>
+t0 :: Source src => LenInj vs => KindInj (K t) =>
       Type src (Proxy t ': vs) t
 t0 = tyVar "t" $ varZ
 
-t1 :: Source src => Inj_Len vs => Inj_Kind (K t) =>
+t1 :: Source src => LenInj vs => KindInj (K t) =>
       Type src (a ': Proxy t ': vs) t
 t1 = tyVar "t" $ VarS varZ
 
-t2 :: Source src => Inj_Len vs => Inj_Kind (K t) =>
+t2 :: Source src => LenInj vs => KindInj (K t) =>
       Type src (a ': b ': Proxy t ': vs) t
 t2 = tyVar "t" $ VarS $ VarS varZ
 
@@ -282,7 +284,7 @@
 teFoldable_foldMap :: TermDef Foldable '[Proxy a, Proxy t, Proxy m] (Foldable t # Monoid m #> ((a -> m) -> t a -> m))
 teFoldable_foldMap = Term (tyFoldable t1 # tyMonoid m) ((a0 ~> m) ~> t1 `tyApp` a0 ~> m) $ teSym @Foldable $ lam2 foldMap
 	where
-	m :: Source src => Inj_Len vs => Inj_Kind (K m) =>
+	m :: Source src => LenInj vs => KindInj (K m) =>
 	     Type src (a ': b ': Proxy m ': vs) m
 	m = tyVar "m" $ VarS $ VarS varZ
 
@@ -330,7 +332,7 @@
 
 {- TODO: when MonadPlus will be supported
 teFoldable_msum ::
- Source src => Inj_Sym ss Foldable =>
+ Source src => SymInj ss Foldable =>
  Term src ss ts '[Proxy a, Proxy t, Proxy f] ((Foldable t # MonadPlus f) #> (t (f a) -> f a))
 teFoldable_msum =
 	Term ((tyFoldable t1 # (tyConst @(K MonadPlus) @MonadPlus `tyApp` f2))) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $
diff --git a/Language/Symantic/Lib/Function.hs b/Language/Symantic/Lib/Function.hs
--- a/Language/Symantic/Lib/Function.hs
+++ b/Language/Symantic/Lib/Function.hs
@@ -10,7 +10,7 @@
 import Language.Symantic
 
 -- * Class 'Sym_Function'
-type instance Sym (Proxy (->)) = Sym_Function
+type instance Sym (->) = Sym_Function
 class Sym_Function term where
 	comp  :: term (b -> c) -> term (a -> b) -> term (a -> c); infixr 9 `comp`
 	const :: term a -> term b -> term a
@@ -46,6 +46,8 @@
 instance (Sym_Function term, Sym_Lambda term) => Sym_Function (BetaT term)
 
 -- Typing
+instance NameTyOf (->) where
+	nameTyOf _c = [] `Mod` "->"
 instance ClassInstancesFor (->) where
 	proveConstraintFor _c (TyApp _ q (TyApp _ z _r))
 	 | Just HRefl <- proj_ConstKiTy @_ @(->) z
@@ -66,7 +68,7 @@
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g (->)
-instance (Source src, Inj_Sym ss (->)) => ModuleFor src ss (->) where
+instance (Source src, SymInj ss (->)) => ModuleFor src ss (->) where
 	moduleFor = ["Function"] `moduleWhere`
 	 [ "const" := teFunction_const
 	 , "flip"  := teFunction_flip
@@ -76,18 +78,18 @@
 	 ]
 
 -- ** 'Type's
-tyFun :: Source src => Inj_Len vs => Type src vs (->)
+tyFun :: Source src => LenInj vs => Type src vs (->)
 tyFun = tyConst @(K (->)) @(->)
 
-a0 :: Source src => Inj_Len vs => Inj_Kind (K a) =>
+a0 :: Source src => LenInj vs => KindInj (K a) =>
      Type src (Proxy a ': vs) a
 a0 = tyVar "a" varZ
 
-b1 :: Source src => Inj_Len vs => Inj_Kind (K b) =>
+b1 :: Source src => LenInj vs => KindInj (K b) =>
      Type src (a ': Proxy b ': vs) b
 b1 = tyVar "b" $ VarS varZ
 
-c2 :: Source src => Inj_Len vs => Inj_Kind (K c) =>
+c2 :: Source src => LenInj vs => KindInj (K c) =>
      Type src (a ': b ': Proxy c ': vs) c
 c2 = tyVar "c" $ VarS $ VarS varZ
 
diff --git a/Language/Symantic/Lib/Functor.hs b/Language/Symantic/Lib/Functor.hs
--- a/Language/Symantic/Lib/Functor.hs
+++ b/Language/Symantic/Lib/Functor.hs
@@ -13,7 +13,7 @@
 import Language.Symantic.Lib.Function (a0, b1)
 
 -- * Class 'Sym_Functor'
-type instance Sym (Proxy Functor) = Sym_Functor
+type instance Sym Functor = Sym_Functor
 class Sym_Functor term where
 	fmap :: Functor f => term (a -> b) -> term (f a) -> term (f b)
 	default fmap :: Sym_Functor (UnT term) => Trans term => Functor f => term (a -> b) -> term (f a) -> term (f b)
@@ -44,13 +44,15 @@
 	(<$)  = trans2 (<$)
 
 -- Typing
+instance NameTyOf Functor where
+	nameTyOf _c = ["Functor"] `Mod` "Functor"
 instance FixityOf Functor
 instance ClassInstancesFor Functor
 instance TypeInstancesFor Functor
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Functor
-instance (Source src, Inj_Sym ss Functor) => ModuleFor src ss Functor where
+instance (Source src, SymInj ss Functor) => ModuleFor src ss Functor where
 	moduleFor = ["Functor"] `moduleWhere`
 	 [ "fmap" := teFunctor_fmap
 	 , "<$"  `withInfixL` 4 := teFunctor_const
@@ -61,11 +63,11 @@
 tyFunctor :: Source src => Type src vs a -> Type src vs (Functor a)
 tyFunctor a = tyConstLen @(K Functor) @Functor (lenVars a) `tyApp` a
 
-f1 :: Source src => Inj_Len vs => Inj_Kind (K f) =>
+f1 :: Source src => LenInj vs => KindInj (K f) =>
       Type src (a ': Proxy f ': vs) f
 f1 = tyVar "f" $ VarS varZ
 
-f2 :: Source src => Inj_Len vs => Inj_Kind (K f) =>
+f2 :: Source src => LenInj vs => KindInj (K f) =>
       Type src (a ': b ': Proxy f ': vs) f
 f2 = tyVar "f" $ VarS $ VarS varZ
 
diff --git a/Language/Symantic/Lib/IO.hs b/Language/Symantic/Lib/IO.hs
--- a/Language/Symantic/Lib/IO.hs
+++ b/Language/Symantic/Lib/IO.hs
@@ -12,9 +12,9 @@
 import Language.Symantic.Lib.Unit (tyUnit)
 
 -- * Class 'Sym_IO'
-type instance Sym (Proxy IO)        = Sym_IO
-type instance Sym (Proxy IO.Handle) = Sym_IO_Handle
-type instance Sym (Proxy IO.IOMode) = Sym_IO_Mode
+type instance Sym IO        = Sym_IO
+type instance Sym IO.Handle = Sym_IO_Handle
+type instance Sym IO.IOMode = Sym_IO_Mode
 class Sym_IO (term:: * -> *)
 class Sym_IO_Handle (term:: * -> *) where
 	io_hClose   :: term IO.Handle -> term (IO ())
@@ -52,6 +52,12 @@
 instance (Sym_IO_Mode term, Sym_Lambda term) => Sym_IO_Mode (BetaT term)
 
 -- Typing
+instance NameTyOf IO where
+	nameTyOf _c = ["IO"] `Mod` "IO"
+instance NameTyOf IO.Handle where
+	nameTyOf _c = ["IO"] `Mod` "Handle"
+instance NameTyOf IO.IOMode where
+	nameTyOf _c = ["IO"] `Mod` "IOMode"
 instance FixityOf IO
 instance ClassInstancesFor IO where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
@@ -94,7 +100,7 @@
 
 -- Compiling
 instance ModuleFor src ss IO
-instance (Source src, Inj_Sym ss IO.Handle) => ModuleFor src ss IO.Handle where
+instance (Source src, SymInj ss IO.Handle) => ModuleFor src ss IO.Handle where
 	moduleFor = ["IO"] `moduleWhere`
 	 [ "hClose"   := teIO_hClose
 	 , "openFile" := teIO_openFile
@@ -108,13 +114,13 @@
 tyIO :: Source src => Type src vs a -> Type src vs (IO a)
 tyIO a = tyConstLen @(K IO) @IO (lenVars a) `tyApp` a
 
-tyIO_Handle :: Source src => Inj_Len vs => Type src vs IO.Handle
+tyIO_Handle :: Source src => LenInj vs => Type src vs IO.Handle
 tyIO_Handle = tyConst @(K IO.Handle) @IO.Handle
 
-tyIO_Mode :: Source src => Inj_Len vs => Type src vs IO.IOMode
+tyIO_Mode :: Source src => LenInj vs => Type src vs IO.IOMode
 tyIO_Mode = tyConst @(K IO.IOMode) @IO.IOMode
 
-tyFilePath :: Source src => Inj_Len vs => Type src vs FilePath
+tyFilePath :: Source src => LenInj vs => Type src vs FilePath
 tyFilePath = tyString
 
 -- ** 'Term's
diff --git a/Language/Symantic/Lib/If.hs b/Language/Symantic/Lib/If.hs
--- a/Language/Symantic/Lib/If.hs
+++ b/Language/Symantic/Lib/If.hs
@@ -13,7 +13,7 @@
 data If
 
 -- * Class 'Sym_If'
-type instance Sym (Proxy If) = Sym_If
+type instance Sym If = Sym_If
 class Sym_If term where
 	if_ :: term Bool -> term a -> term a -> term a
 	default if_ :: Sym_If (UnT term) => Trans term => term Bool -> term a -> term a -> term a
@@ -38,6 +38,8 @@
 instance (Sym_If term, Sym_Lambda term) => Sym_If (BetaT term)
 
 -- Typing
+instance NameTyOf If where
+	nameTyOf _c = ["If"] `Mod` "If"
 instance ClassInstancesFor If
 instance TypeInstancesFor If
 
diff --git a/Language/Symantic/Lib/Int.hs b/Language/Symantic/Lib/Int.hs
--- a/Language/Symantic/Lib/Int.hs
+++ b/Language/Symantic/Lib/Int.hs
@@ -8,7 +8,7 @@
 import Language.Symantic
 
 -- * Class 'Sym_Int'
-type instance Sym (Proxy Int) = Sym_Int
+type instance Sym Int = Sym_Int
 class Sym_Int term where
 	int :: Int -> term Int
 	default int :: Sym_Int (UnT term) => Trans term => Int -> term Int
@@ -27,6 +27,8 @@
 instance (Sym_Int term, Sym_Lambda term) => Sym_Int (BetaT term)
 
 -- Typing
+instance NameTyOf Int where
+	nameTyOf _c = ["Int"] `Mod` "Int"
 instance ClassInstancesFor Int where
 	proveConstraintFor _c (TyApp _ (TyConst _ _ q) z)
 	 | Just HRefl <- proj_ConstKiTy @_ @Int z
@@ -48,9 +50,9 @@
 instance ModuleFor src ss Int
 
 -- ** 'Type's
-tyInt :: Source src => Inj_Len vs => Type src vs Int
+tyInt :: Source src => LenInj vs => Type src vs Int
 tyInt = tyConst @(K Int) @Int
 
 -- ** 'Term's
-teInt :: Source src => Inj_Sym ss Int => Int -> Term src ss ts '[] (() #> Int)
+teInt :: Source src => SymInj ss Int => Int -> Term src ss ts '[] (() #> Int)
 teInt i = Term noConstraint tyInt $ teSym @Int $ int i
diff --git a/Language/Symantic/Lib/Integer.hs b/Language/Symantic/Lib/Integer.hs
--- a/Language/Symantic/Lib/Integer.hs
+++ b/Language/Symantic/Lib/Integer.hs
@@ -9,7 +9,7 @@
 import Language.Symantic.Grammar
 
 -- * Class 'Sym_Integer'
-type instance Sym (Proxy Integer) = Sym_Integer
+type instance Sym Integer = Sym_Integer
 class Sym_Integer term where
 	integer :: Integer -> term Integer
 	default integer :: Sym_Integer (UnT term) => Trans term => Integer -> term Integer
@@ -28,6 +28,8 @@
 instance (Sym_Integer term, Sym_Lambda term) => Sym_Integer (BetaT term)
 
 -- Typing
+instance NameTyOf Integer where
+	nameTyOf _c = ["Integer"] `Mod` "Integer"
 instance ClassInstancesFor Integer where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
 	 | Just HRefl <- proj_ConstKiTy @_ @Integer z
@@ -50,19 +52,19 @@
  , Gram_AltApp g
  , Gram_Rule g
  , Gram_Comment g
- , Inj_Sym ss Integer
+ , SymInj ss Integer
  ) => Gram_Term_AtomsFor src ss g Integer where
 	g_term_atomsFor =
 	 [ rule "teinteger" $
-		lexeme $ g_source $
+		lexeme $ source $
 		(\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i)
 		 <$> some (choice $ char <$> ['0'..'9'])
 	 ]
 instance ModuleFor src ss Integer
 
 -- ** 'Term's
-tyInteger :: Source src => Inj_Len vs => Type src vs Integer
+tyInteger :: Source src => LenInj vs => Type src vs Integer
 tyInteger = tyConst @(K Integer) @Integer
 
-teInteger :: Source src => Inj_Sym ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
+teInteger :: Source src => SymInj ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
 teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i
diff --git a/Language/Symantic/Lib/Integral.hs b/Language/Symantic/Lib/Integral.hs
--- a/Language/Symantic/Lib/Integral.hs
+++ b/Language/Symantic/Lib/Integral.hs
@@ -13,7 +13,7 @@
 import Language.Symantic.Lib.Tuple2 (tyTuple2)
 
 -- * Class 'Sym_Integral'
-type instance Sym (Proxy Integral) = Sym_Integral
+type instance Sym Integral = Sym_Integral
 class Sym_Integral term where
 	quot      :: Integral i => term i -> term i -> term i; infixl 7 `quot`
 	rem       :: Integral i => term i -> term i -> term i; infixl 7 `rem`
@@ -69,13 +69,15 @@
 instance (Sym_Integral term, Sym_Lambda term) => Sym_Integral (BetaT term)
 
 -- Typing
+instance NameTyOf Integral where
+	nameTyOf _c = ["Integral"] `Mod` "Integral"
 instance FixityOf Integral
 instance ClassInstancesFor Integral
 instance TypeInstancesFor Integral
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Integral
-instance (Source src, Inj_Sym ss Integral) => ModuleFor src ss Integral where
+instance (Source src, SymInj ss Integral) => ModuleFor src ss Integral where
 	moduleFor = ["Integral"] `moduleWhere`
 	 [ "quot" `withInfixL` 7 := teIntegral_quot
 	 , "rem"  `withInfixL` 7 := teIntegral_rem
diff --git a/Language/Symantic/Lib/List.hs b/Language/Symantic/Lib/List.hs
--- a/Language/Symantic/Lib/List.hs
+++ b/Language/Symantic/Lib/List.hs
@@ -13,12 +13,12 @@
 import qualified Data.Traversable as Traversable
 
 import Language.Symantic
-import Language.Symantic.Grammar
+import Language.Symantic.Grammar as G
 import Language.Symantic.Lib.Function (a0, b1, c2)
 import Language.Symantic.Lib.MonoFunctor (Element)
 
 -- * Class 'Sym_List'
-type instance Sym (Proxy []) = Sym_List
+type instance Sym [] = Sym_List
 class Sym_List term where
 	list_empty :: term [a]
 	list_cons  :: term a -> term [a] -> term [a]; infixr 5 `list_cons`
@@ -62,7 +62,9 @@
 instance (Sym_List term, Sym_Lambda term) => Sym_List (BetaT term)
 
 -- Typing
-instance FixityOf [] where
+instance NameTyOf [] where
+	nameTyOf _c = [] `Mod` "[]"
+instance FixityOf []
 instance ClassInstancesFor [] where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
 	 | Just HRefl <- proj_ConstKiTy @_ @[] z
@@ -102,13 +104,13 @@
  , Gram_Rule g
  , Gram_Comment g
  , Gram_Term src ss g
- , Inj_Sym ss []
+ , SymInj ss []
  ) => Gram_Term_AtomsFor src ss g [] where
 	g_term_atomsFor =
 	 [ rule "teList_list" $
 		between (symbol "[") (symbol "]") listG
 	 , rule "teList_empty" $
-		g_source $
+		G.source $
 		(\src -> BinTree0 $ Token_Term $ TermAVT teList_empty `setSource` src)
 		 <$ symbol "["
 		 <* symbol "]"
@@ -116,7 +118,7 @@
 		where
 		listG :: CF g (AST_Term src ss)
 		listG = rule "list" $
-			g_source $
+			G.source $
 			(\a mb src ->
 				case mb of
 				 Just b  -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a) b
@@ -126,7 +128,7 @@
 					 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_empty))
 			 <$> g_term
 			 <*> option Nothing (Just <$ symbol "," <*> listG)
-instance (Source src, Inj_Sym ss []) => ModuleFor src ss [] where
+instance (Source src, SymInj ss []) => ModuleFor src ss [] where
 	moduleFor = ["List"] `moduleWhere`
 	 [ "[]"      := teList_empty
 	 , "zipWith" := teList_zipWith
@@ -134,15 +136,15 @@
 	 ]
 
 -- ** 'Type's
-tyList :: Source src => Inj_Len vs => Type src vs a -> Type src vs [a]
+tyList :: Source src => LenInj vs => Type src vs a -> Type src vs [a]
 tyList = (tyConst @(K []) @[] `tyApp`)
 
 -- ** 'Term's
-teList_empty :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a] (() #> [a])
+teList_empty :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> [a])
 teList_empty = Term noConstraint (tyList a0) $ teSym @[] $ list_empty
 
-teList_cons :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a] (() #> (a -> [a] -> [a]))
+teList_cons :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> (a -> [a] -> [a]))
 teList_cons = Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $ teSym @[] $ lam2 list_cons
 
-teList_zipWith :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> [a] -> [b] -> [c]))
+teList_zipWith :: Source src => SymInj ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> [a] -> [b] -> [c]))
 teList_zipWith = Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $ teSym @[] $ lam3 zipWith
diff --git a/Language/Symantic/Lib/Map.hs b/Language/Symantic/Lib/Map.hs
--- a/Language/Symantic/Lib/Map.hs
+++ b/Language/Symantic/Lib/Map.hs
@@ -17,7 +17,7 @@
 import Language.Symantic.Lib.Tuple2 (tyTuple2)
 
 -- * Class 'Sym_Map'
-type instance Sym (Proxy Map) = Sym_Map
+type instance Sym Map = Sym_Map
 class Sym_Map term where
 	map_fromList     :: Ord k => term [(k, a)] -> term (Map k a)
 	map_mapWithKey   :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)
@@ -85,6 +85,8 @@
 instance (Sym_Map term, Sym_Lambda term) => Sym_Map (BetaT term)
 
 -- Typing
+instance NameTyOf Map where
+	nameTyOf _c = ["Map"] `Mod` "Map"
 instance FixityOf Map
 instance ClassInstancesFor Map where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _k))
@@ -120,7 +122,7 @@
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Map
-instance (Source src, Inj_Sym ss Map) => ModuleFor src ss Map where
+instance (Source src, SymInj ss Map) => ModuleFor src ss Map where
 	moduleFor = ["Map"] `moduleWhere`
 	 [ "delete"       := teMap_delete
 	 , "difference"   := teMap_difference
@@ -134,14 +136,14 @@
 	 ]
 
 -- ** 'Type's
-tyMap :: Source src => Inj_Len vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)
+tyMap :: Source src => LenInj vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)
 tyMap k a = tyConst @(K Map) @Map `tyApp` k `tyApp` a
 
-k1 :: Source src => Inj_Len vs => Inj_Kind (K k) =>
+k1 :: Source src => LenInj vs => KindInj (K k) =>
      Type src (a ': Proxy k ': vs) k
 k1 = tyVar "k" $ VarS varZ
 
-k2 :: Source src => Inj_Len vs => Inj_Kind (K k) =>
+k2 :: Source src => LenInj vs => KindInj (K k) =>
      Type src (a ': b ': Proxy k ': vs) k
 k2 = tyVar "k" $ VarS $ VarS varZ
 
diff --git a/Language/Symantic/Lib/Maybe.hs b/Language/Symantic/Lib/Maybe.hs
--- a/Language/Symantic/Lib/Maybe.hs
+++ b/Language/Symantic/Lib/Maybe.hs
@@ -13,7 +13,7 @@
 import Language.Symantic.Lib.MonoFunctor (Element)
 
 -- * Class 'Sym_Maybe'
-type instance Sym (Proxy Maybe) = Sym_Maybe
+type instance Sym Maybe = Sym_Maybe
 class Sym_Maybe term where
 	_Nothing :: term (Maybe a)
 	_Just    :: term a -> term (Maybe a)
@@ -45,6 +45,8 @@
 instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term)
 
 -- Typing
+instance NameTyOf Maybe where
+	nameTyOf _c = ["Maybe"] `Mod` "Maybe"
 instance FixityOf Maybe
 instance ClassInstancesFor Maybe where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
@@ -78,7 +80,7 @@
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Maybe
-instance (Source src, Inj_Sym ss Maybe) => ModuleFor src ss Maybe where
+instance (Source src, SymInj ss Maybe) => ModuleFor src ss Maybe where
 	moduleFor = ["Maybe"] `moduleWhere`
 	 [ "Nothing" := teMaybe_Nothing
 	 , "Just"    := teMaybe_Just
@@ -86,7 +88,7 @@
 	 ]
 
 -- ** 'Type's
-tyMaybe :: Source src => Inj_Len vs => Type src vs a -> Type src vs (Maybe a)
+tyMaybe :: Source src => LenInj vs => Type src vs a -> Type src vs (Maybe a)
 tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)
 
 -- ** 'Term's
diff --git a/Language/Symantic/Lib/Monad.hs b/Language/Symantic/Lib/Monad.hs
--- a/Language/Symantic/Lib/Monad.hs
+++ b/Language/Symantic/Lib/Monad.hs
@@ -14,7 +14,7 @@
 import Language.Symantic.Lib.Bool (tyBool)
 
 -- * Class 'Sym_Monad'
-type instance Sym (Proxy Monad) = Sym_Monad
+type instance Sym Monad = Sym_Monad
 class Sym_Monad term where
 	return :: Monad m       => term a -> term (m a)
 	(>>=)  :: Monad m       => term (m a) -> term (a -> m b) -> term (m b); infixl 1 >>=
@@ -58,13 +58,15 @@
 instance (Sym_Monad term, Sym_Lambda term) => Sym_Monad (BetaT term)
 
 -- Typing
+instance NameTyOf Monad where
+	nameTyOf _c = ["Monad"] `Mod` "Monad"
 instance FixityOf Monad
 instance ClassInstancesFor Monad
 instance TypeInstancesFor Monad
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Monad
-instance (Source src, Inj_Sym ss Monad) => ModuleFor src ss Monad where
+instance (Source src, SymInj ss Monad) => ModuleFor src ss Monad where
 	moduleFor = ["Monad"] `moduleWhere`
 	 [ "return" := teMonad_return
 	 , "join"   := teMonad_join
@@ -77,19 +79,19 @@
 tyMonad :: Source src => Type src vs m -> Type src vs (Monad m)
 tyMonad m = tyConstLen @(K Monad) @Monad (lenVars m) `tyApp` m
 
-m0 :: Source src => Inj_Len vs => Inj_Kind (K m) =>
+m0 :: Source src => LenInj vs => KindInj (K m) =>
      Type src (Proxy m ': vs) m
 m0 = tyVar "m" varZ
 
-m1 :: Source src => Inj_Len vs => Inj_Kind (K m) =>
+m1 :: Source src => LenInj vs => KindInj (K m) =>
      Type src (a ': Proxy m ': vs) m
 m1 = tyVar "m" $ VarS varZ
 
-m2 :: Source src => Inj_Len vs => Inj_Kind (K m) =>
+m2 :: Source src => LenInj vs => KindInj (K m) =>
      Type src (a ': b ': Proxy m ': vs) m
 m2 = tyVar "m" $ VarS $ VarS varZ
 
-m3 :: Source src => Inj_Len vs => Inj_Kind (K m) =>
+m3 :: Source src => LenInj vs => KindInj (K m) =>
      Type src (a ': b ': c ': Proxy m ': vs) m
 m3 = tyVar "m" $ VarS $ VarS $ VarS varZ
 
diff --git a/Language/Symantic/Lib/MonoFoldable.hs b/Language/Symantic/Lib/MonoFoldable.hs
--- a/Language/Symantic/Lib/MonoFoldable.hs
+++ b/Language/Symantic/Lib/MonoFoldable.hs
@@ -15,7 +15,7 @@
 import Language.Symantic.Lib.Monoid (tyMonoid)
 
 -- * Class 'Sym_MonoFoldable'
-type instance Sym (Proxy MonoFoldable) = Sym_MonoFoldable
+type instance Sym MonoFoldable = Sym_MonoFoldable
 class Sym_MonoFoldable term where
 	ofoldMap :: (MonoFoldable o, Monoid m) => term (MT.Element o -> m) -> term o -> term m
 	ofoldr   :: MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b
@@ -75,13 +75,15 @@
 instance (Sym_MonoFoldable term, Sym_Lambda term) => Sym_MonoFoldable (BetaT term)
 
 -- Typing
+instance NameTyOf MonoFoldable where
+	nameTyOf _c = ["MonoFoldable"] `Mod` "MonoFoldable"
 instance FixityOf MonoFoldable
 instance ClassInstancesFor MonoFoldable
 instance TypeInstancesFor MonoFoldable
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g MonoFoldable
-instance (Source src, Inj_Sym ss MonoFoldable) => ModuleFor src ss MonoFoldable where
+instance (Source src, SymInj ss MonoFoldable) => ModuleFor src ss MonoFoldable where
 	moduleFor = ["MonoFoldable"] `moduleWhere`
 	 [ "ofoldMap" := teMonoFoldable_ofoldMap
 	 , "otoList"  := teMonoFoldable_otoList
@@ -101,7 +103,7 @@
 teMonoFoldable_ofoldMap :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy m] (MonoFoldable o # Monoid m # e #~ MT.Element o #> ((e -> m) -> o -> m))
 teMonoFoldable_ofoldMap = Term (tyMonoFoldable o0 # tyMonoid m # e1 #~ famElement o0) ((e1 ~> m) ~> o0 ~> m) $ teSym @MonoFoldable $ lam2 ofoldMap
 	where
-	m :: Source src => Inj_Len vs => Inj_Kind (K m) => Type src (Proxy a ': Proxy b ': Proxy m ': vs) m
+	m :: Source src => LenInj vs => KindInj (K m) => Type src (Proxy a ': Proxy b ': Proxy m ': vs) m
 	m = tyVar "m" $ VarS $ VarS varZ
 
 teMonoFoldable_otoList :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (o -> [MT.Element o]))
@@ -110,13 +112,13 @@
 teMonoFoldable_ofoldr :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy a] (MonoFoldable o # e #~ MT.Element o #> ((e -> a -> a) -> a -> o -> a))
 teMonoFoldable_ofoldr = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> a ~> a) ~> a ~> o0 ~> a) $ teSym @MonoFoldable $ lam1 $ \f -> lam $ lam . ofoldr f
 	where
-	a :: Source src => Inj_Len vs => Inj_Kind (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a
+	a :: Source src => LenInj vs => KindInj (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a
 	a = tyVar "a" $ VarS $ VarS varZ
 
 teMonoFoldable_ofoldl' :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy a] (MonoFoldable o # e #~ MT.Element o #> ((a -> e -> a) -> a -> o -> a))
 teMonoFoldable_ofoldl' = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((a ~> e1 ~> a) ~> a ~> o0 ~> a) $ teSym @MonoFoldable $ lam1 $ \f -> lam $ lam . ofoldl' f
 	where
-	a :: Source src => Inj_Len vs => Inj_Kind (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a
+	a :: Source src => LenInj vs => KindInj (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a
 	a = tyVar "a" $ VarS $ VarS varZ
 
 teMonoFoldable_olength :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (o -> Int))
diff --git a/Language/Symantic/Lib/MonoFunctor.hs b/Language/Symantic/Lib/MonoFunctor.hs
--- a/Language/Symantic/Lib/MonoFunctor.hs
+++ b/Language/Symantic/Lib/MonoFunctor.hs
@@ -12,6 +12,8 @@
 -- * Type 'Element'
 data Element
 type instance Fam Element '[h] = MT.Element (UnProxy h)
+instance NameTyOf Element where
+	nameTyOf _c = ["MonoFunctor"] `Mod` "Element"
 instance ClassInstancesFor Element
 instance TypeInstancesFor Element where
 	expandFamFor _c _len f (TyApp _ (TyApp _ z _ty_r) a `TypesS` TypesZ)
@@ -22,10 +24,10 @@
 
 -- ** 'Type's
 famElement :: Source src => Type src vs t -> Type src vs (MT.Element t)
-famElement o = TyFam noSource (lenVars o) (inj_Const @Element) (o `TypesS` TypesZ)
+famElement o = TyFam noSource (lenVars o) (constInj @Element) (o `TypesS` TypesZ)
 
 -- * Class 'Sym_MonoFunctor'
-type instance Sym (Proxy MonoFunctor) = Sym_MonoFunctor
+type instance Sym MonoFunctor = Sym_MonoFunctor
 class Sym_MonoFunctor term where
 	omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
 	default omap
@@ -47,13 +49,15 @@
 instance (Sym_MonoFunctor term, Sym_Lambda term) => Sym_MonoFunctor (BetaT term)
 
 -- Typing
+instance NameTyOf MonoFunctor where
+	nameTyOf _c = ["MonoFunctor"] `Mod` "MonoFunctor"
 instance FixityOf MonoFunctor
 instance ClassInstancesFor MonoFunctor
 instance TypeInstancesFor MonoFunctor
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g MonoFunctor
-instance (Source src, Inj_Sym ss MonoFunctor) => ModuleFor src ss MonoFunctor where
+instance (Source src, SymInj ss MonoFunctor) => ModuleFor src ss MonoFunctor where
 	moduleFor = ["MonoFunctor"] `moduleWhere`
 	 [ "omap" := teMonoFunctor_omap
 	 ]
@@ -62,11 +66,11 @@
 tyMonoFunctor :: Source src => Type src vs a -> Type src vs (MonoFunctor a)
 tyMonoFunctor a = tyConstLen @(K MonoFunctor) @MonoFunctor (lenVars a) `tyApp` a
 
-o0 :: Source src => Inj_Len vs => Inj_Kind (K o) =>
+o0 :: Source src => LenInj vs => KindInj (K o) =>
      Type src (Proxy o ': vs) o
 o0 = tyVar "o" varZ
 
-e1 :: Source src => Inj_Len vs => Inj_Kind (K e) =>
+e1 :: Source src => LenInj vs => KindInj (K e) =>
      Type src (a ': Proxy e ': vs) e
 e1 = tyVar "e" $ VarS varZ
 
diff --git a/Language/Symantic/Lib/Monoid.hs b/Language/Symantic/Lib/Monoid.hs
--- a/Language/Symantic/Lib/Monoid.hs
+++ b/Language/Symantic/Lib/Monoid.hs
@@ -11,7 +11,7 @@
 import Language.Symantic.Lib.Function (a0)
 
 -- * Class 'Sym_Monoid'
-type instance Sym (Proxy Monoid) = Sym_Monoid
+type instance Sym Monoid = Sym_Monoid
 class Sym_Monoid term where
 	mempty  :: Monoid a => term a
 	mappend :: Monoid a => term a -> term a -> term a
@@ -35,13 +35,15 @@
 instance (Sym_Monoid term, Sym_Lambda term) => Sym_Monoid (BetaT term)
 
 -- Typing
+instance NameTyOf Monoid where
+	nameTyOf _c = ["Monoid"] `Mod` "Monoid"
 instance FixityOf Monoid
 instance ClassInstancesFor Monoid
 instance TypeInstancesFor Monoid
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Monoid
-instance (Source src, Inj_Sym ss Monoid) => ModuleFor src ss Monoid where
+instance (Source src, SymInj ss Monoid) => ModuleFor src ss Monoid where
 	moduleFor = ["Monoid"] `moduleWhere`
 	 [ "mempty"  := teMonoid_mempty
 	 , "mappend" := teMonoid_mappend
diff --git a/Language/Symantic/Lib/NonNull.hs b/Language/Symantic/Lib/NonNull.hs
--- a/Language/Symantic/Lib/NonNull.hs
+++ b/Language/Symantic/Lib/NonNull.hs
@@ -19,7 +19,7 @@
 import Language.Symantic.Lib.Tuple2 (tyTuple2)
 
 -- * Class 'Sym_NonNull'
-type instance Sym (Proxy NonNull) = Sym_NonNull
+type instance Sym NonNull = Sym_NonNull
 class Sym_NonNull term where
 	fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
 	toNullable   :: MonoFoldable o => term (NonNull o) -> term o
@@ -85,6 +85,8 @@
 instance (Sym_NonNull term, Sym_Lambda term) => Sym_NonNull (BetaT term)
 
 -- Typing
+instance NameTyOf NonNull where
+	nameTyOf _c = ["NonNull"] `Mod` "NonNull"
 instance FixityOf NonNull
 instance TypeInstancesFor NonNull where
 	expandFamFor c len f (TyApp _ z o `TypesS` TypesZ)
@@ -113,7 +115,7 @@
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g NonNull
-instance (Source src, Inj_Sym ss NonNull) => ModuleFor src ss NonNull where
+instance (Source src, SymInj ss NonNull) => ModuleFor src ss NonNull where
 	moduleFor = ["NonNull"] `moduleWhere`
 	 [ "fromNullable" := teNonNull_fromNullable
 	 , "toNullable"   := teNonNull_toNullable
diff --git a/Language/Symantic/Lib/Num.hs b/Language/Symantic/Lib/Num.hs
--- a/Language/Symantic/Lib/Num.hs
+++ b/Language/Symantic/Lib/Num.hs
@@ -12,7 +12,7 @@
 import Language.Symantic.Lib.Integer (tyInteger)
 
 -- * Class 'Sym_Num'
-type instance Sym (Proxy Num) = Sym_Num
+type instance Sym Num = Sym_Num
 class Sym_Num term where
 	abs         :: Num n => term n -> term n
 	negate      :: Num n => term n -> term n
@@ -68,13 +68,15 @@
 instance (Sym_Num term, Sym_Lambda term) => Sym_Num (BetaT term)
 
 -- Typing
+instance NameTyOf Num where
+	nameTyOf _c = ["Num"] `Mod` "Num"
 instance FixityOf Num
 instance ClassInstancesFor Num
 instance TypeInstancesFor Num
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Num
-instance (Source src, Inj_Sym ss Num) => ModuleFor src ss Num where
+instance (Source src, SymInj ss Num) => ModuleFor src ss Num where
 	moduleFor = ["Num"] `moduleWhere`
 	 [ "abs"    := teNum_abs
 	 , "negate" := teNum_negate
diff --git a/Language/Symantic/Lib/Num/Test.hs b/Language/Symantic/Lib/Num/Test.hs
--- a/Language/Symantic/Lib/Num/Test.hs
+++ b/Language/Symantic/Lib/Num/Test.hs
@@ -76,18 +76,20 @@
 
 -- | A newtype to test prefix and postfix.
 newtype Num2 a = Num2 a
-type instance Sym (Proxy Num2) = Sym_Num2
+type instance Sym Num2 = Sym_Num2
 class Sym_Num2 (term:: * -> *) where
 
 instance Sym_Num2 Eval where
 instance Sym_Num2 View where
 instance Sym_Num2 (Dup r1 r2) where
 instance Sym_Num2 term => Sym_Num2 (BetaT term) where
+instance NameTyOf Num2 where
+	nameTyOf _c = ["Num2"] `Mod` "Num2"
 instance FixityOf Num2
 instance ClassInstancesFor Num2
 instance TypeInstancesFor Num2
 instance Gram_Term_AtomsFor src ss g Num2
-instance (Source src, Inj_Sym ss Num) => ModuleFor src ss Num2 where
+instance (Source src, SymInj ss Num) => ModuleFor src ss Num2 where
 	moduleFor = ["Num2"] `moduleWhere`
 	 [ "abs"    `withPrefix`   9 := teNum_abs
 	 , "negate" `withPrefix`  10 := teNum_negate
diff --git a/Language/Symantic/Lib/Ord.hs b/Language/Symantic/Lib/Ord.hs
--- a/Language/Symantic/Lib/Ord.hs
+++ b/Language/Symantic/Lib/Ord.hs
@@ -14,7 +14,7 @@
 import Language.Symantic.Lib.Eq (Sym_Eq)
 
 -- * Class 'Sym_Ordering'
-type instance Sym (Proxy Ordering) = Sym_Ordering
+type instance Sym Ordering = Sym_Ordering
 class Sym_Eq term => Sym_Ordering term where
 	ordering :: Ordering -> term Ordering
 	default ordering :: Sym_Ordering (UnT term) => Trans term => Ordering -> term Ordering
@@ -33,12 +33,14 @@
 instance (Sym_Ordering term, Sym_Lambda term) => Sym_Ordering (BetaT term)
 
 -- Typing
+instance NameTyOf Ordering where
+	nameTyOf _c = ["Ord"] `Mod` "Ordering"
 instance ClassInstancesFor Ordering
 instance TypeInstancesFor Ordering
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Ordering
-instance (Source src, Inj_Sym ss Ordering) => ModuleFor src ss Ordering where
+instance (Source src, SymInj ss Ordering) => ModuleFor src ss Ordering where
 	moduleFor = [] `moduleWhere`
 	 [ "LT" := teOrdering LT
 	 , "EQ" := teOrdering EQ
@@ -46,15 +48,15 @@
 	 ]
 
 -- ** 'Type's
-tyOrdering :: Source src => Inj_Len vs => Type src vs Ordering
+tyOrdering :: Source src => LenInj vs => Type src vs Ordering
 tyOrdering = tyConst @(K Ordering) @Ordering
 
 -- ** 'Term's
-teOrdering :: Source src => Inj_Sym ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)
+teOrdering :: Source src => SymInj ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)
 teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o
 
 -- * Class 'Sym_Ord'
-type instance Sym (Proxy Ord) = Sym_Ord
+type instance Sym Ord = Sym_Ord
 class Sym_Eq term => Sym_Ord term where
 	compare  :: Ord a => term a -> term a -> term Ordering
 	(<)      :: Ord a => term a -> term a -> term Bool; infix 4 <
@@ -110,6 +112,8 @@
 instance (Sym_Ord term, Sym_Lambda term) => Sym_Ord (BetaT term)
 
 -- Typing
+instance NameTyOf Ord where
+	nameTyOf _c = ["Ord"] `Mod` "Ord"
 instance FixityOf Ord
 instance ClassInstancesFor Ord where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
@@ -126,7 +130,7 @@
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Ord
-instance (Source src, Inj_Sym ss Ord) => ModuleFor src ss Ord where
+instance (Source src, SymInj ss Ord) => ModuleFor src ss Ord where
 	moduleFor = ["Ord"] `moduleWhere`
 	 [ "compare" := teOrd_compare
 	 , "<"  `withInfixN` 4 := teOrd_lt
diff --git a/Language/Symantic/Lib/Ratio.hs b/Language/Symantic/Lib/Ratio.hs
--- a/Language/Symantic/Lib/Ratio.hs
+++ b/Language/Symantic/Lib/Ratio.hs
@@ -11,7 +11,7 @@
 import Language.Symantic.Lib.Integral (tyIntegral)
 
 -- * Class 'Sym_Ratio'
-type instance Sym (Proxy Ratio) = Sym_Ratio
+type instance Sym Ratio = Sym_Ratio
 class Sym_Ratio term where
 	ratio       :: Integral a => term a -> term a -> term (Ratio a)
 	numerator   :: term (Ratio a) -> term a
@@ -43,6 +43,8 @@
 instance (Sym_Ratio term, Sym_Lambda term) => Sym_Ratio (BetaT term)
 
 -- Typing
+instance NameTyOf Ratio where
+	nameTyOf _c = ["Ratio"] `Mod` "Ratio"
 instance FixityOf Ratio
 instance ClassInstancesFor Ratio where
 	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
@@ -68,7 +70,7 @@
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Ratio
-instance (Source src, Inj_Sym ss Ratio) => ModuleFor src ss Ratio where
+instance (Source src, SymInj ss Ratio) => ModuleFor src ss Ratio where
 	moduleFor = ["Ratio"] `moduleWhere`
 	 [ "ratio"       := teRatio
 	 , "numerator"   := teRatio_numerator
diff --git a/Language/Symantic/Lib/Real.hs b/Language/Symantic/Lib/Real.hs
--- a/Language/Symantic/Lib/Real.hs
+++ b/Language/Symantic/Lib/Real.hs
@@ -13,7 +13,7 @@
 import Language.Symantic.Lib.Ratio (tyRatio)
 
 -- * Class 'Sym_Real'
-type instance Sym (Proxy Real) = Sym_Real
+type instance Sym Real = Sym_Real
 class Sym_Real term where
 	toRational :: Real a => term a -> term Rational
 	default toRational :: Sym_Real (UnT term) => Trans term => Real a => term a -> term Rational
@@ -31,13 +31,15 @@
 instance (Sym_Real term, Sym_Lambda term) => Sym_Real (BetaT term)
 
 -- Typing
+instance NameTyOf Real where
+	nameTyOf _c = ["Real"] `Mod` "Real"
 instance FixityOf Real
 instance ClassInstancesFor Real
 instance TypeInstancesFor Real
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Real
-instance (Source src, Inj_Sym ss Real) => ModuleFor src ss Real where
+instance (Source src, SymInj ss Real) => ModuleFor src ss Real where
 	moduleFor = ["Real"] `moduleWhere`
 	 [ "toRational" := teReal_toRational
 	 ]
@@ -46,7 +48,7 @@
 tyReal :: Source src => Type src vs a -> Type src vs (Real a)
 tyReal a = tyConstLen @(K Real) @Real (lenVars a) `tyApp` a
 
-tyRational :: Source src => Inj_Len vs => Type src vs Rational
+tyRational :: Source src => LenInj vs => Type src vs Rational
 tyRational = tyRatio tyInteger
 
 -- ** 'Term's
diff --git a/Language/Symantic/Lib/Semigroup.hs b/Language/Symantic/Lib/Semigroup.hs
--- a/Language/Symantic/Lib/Semigroup.hs
+++ b/Language/Symantic/Lib/Semigroup.hs
@@ -11,7 +11,7 @@
 import Language.Symantic.Lib.Integral (tyIntegral)
 
 -- * Class 'Sym_Semigroup'
-type instance Sym (Proxy Semigroup) = Sym_Semigroup
+type instance Sym Semigroup = Sym_Semigroup
 class Sym_Semigroup term where
 	(<>)   :: Semigroup a => term a -> term a -> term a
 	stimes :: (Semigroup a, Integral b) => term b -> term a -> term a
@@ -36,13 +36,15 @@
 instance (Sym_Semigroup term, Sym_Lambda term) => Sym_Semigroup (BetaT term)
 
 -- Typing
+instance NameTyOf Semigroup where
+	nameTyOf _c = ["Semigroup"] `Mod` "Semigroup"
 instance FixityOf Semigroup
 instance ClassInstancesFor Semigroup
 instance TypeInstancesFor Semigroup
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Semigroup
-instance (Source src, Inj_Sym ss Semigroup) => ModuleFor src ss Semigroup where
+instance (Source src, SymInj ss Semigroup) => ModuleFor src ss Semigroup where
 	moduleFor = ["Semigroup"] `moduleWhere`
 	 [ "<>" `withInfixR` 6 := teSemigroup_sappend
 	 , "stimes" := teSemigroup_stimes
diff --git a/Language/Symantic/Lib/Sequences.hs b/Language/Symantic/Lib/Sequences.hs
--- a/Language/Symantic/Lib/Sequences.hs
+++ b/Language/Symantic/Lib/Sequences.hs
@@ -14,7 +14,7 @@
 import Language.Symantic.Lib.MonoFunctor (e1, famElement)
 
 -- * Class 'Sym_SemiSequence'
-type instance Sym (Proxy SemiSequence) = Sym_SemiSequence
+type instance Sym SemiSequence = Sym_SemiSequence
 class Sym_SemiSequence term where
 	intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s
 	cons        :: SemiSequence s => term (MT.Element s) -> term s -> term s
@@ -50,13 +50,15 @@
 instance (Sym_SemiSequence term, Sym_Lambda term) => Sym_SemiSequence (BetaT term)
 
 -- Typing
+instance NameTyOf SemiSequence where
+	nameTyOf _c = ["SemiSequence"] `Mod` "SemiSequence"
 instance FixityOf SemiSequence
 instance ClassInstancesFor SemiSequence
 instance TypeInstancesFor SemiSequence
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g SemiSequence
-instance (Source src, Inj_Sym ss SemiSequence) => ModuleFor src ss SemiSequence where
+instance (Source src, SymInj ss SemiSequence) => ModuleFor src ss SemiSequence where
 	moduleFor = ["SemiSequence"] `moduleWhere`
 	 [ "intersperse" := teSemiSequence_intersperse
 	 , "cons"        := teSemiSequence_cons
@@ -68,7 +70,7 @@
 tySemiSequence :: Source src => Type src vs a -> Type src vs (SemiSequence a)
 tySemiSequence a = tyConstLen @(K SemiSequence) @SemiSequence (lenVars a) `tyApp` a
 
-s0 :: Source src => Inj_Len vs => Inj_Kind (K s) =>
+s0 :: Source src => LenInj vs => KindInj (K s) =>
       Type src (Proxy s ': vs) s
 s0 = tyVar "s" varZ
 
@@ -84,7 +86,7 @@
 teSemiSequence_snoc = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> e1 ~> s0) $ teSym @SemiSequence $ lam2 snoc
 
 -- * Class 'Sym_IsSequence'
-type instance Sym (Proxy IsSequence) = Sym_IsSequence
+type instance Sym IsSequence = Sym_IsSequence
 class Sym_IsSequence term where
 	filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
 	default filter :: Sym_IsSequence (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
@@ -102,13 +104,15 @@
 instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)
 
 -- Typing
+instance NameTyOf IsSequence where
+	nameTyOf _c = ["IsSequence"] `Mod` "IsSequence"
 instance FixityOf IsSequence
 instance ClassInstancesFor IsSequence
 instance TypeInstancesFor IsSequence
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g IsSequence
-instance (Source src, Inj_Sym ss IsSequence) => ModuleFor src ss IsSequence where
+instance (Source src, SymInj ss IsSequence) => ModuleFor src ss IsSequence where
 	moduleFor = ["IsSequence"] `moduleWhere`
 	 [ "filter" := teIsSequence_filter
 	 ]
diff --git a/Language/Symantic/Lib/Show.hs b/Language/Symantic/Lib/Show.hs
--- a/Language/Symantic/Lib/Show.hs
+++ b/Language/Symantic/Lib/Show.hs
@@ -14,7 +14,7 @@
 import Language.Symantic.Lib.List (tyList)
 
 -- * Class 'Sym_Show'
-type instance Sym (Proxy Show) = Sym_Show
+type instance Sym Show = Sym_Show
 class Sym_Show term where
 	showsPrec :: Show a => term Int -> term a -> term ShowS
 	show      :: Show a => term a -> term String
@@ -45,13 +45,15 @@
 instance (Sym_Show term, Sym_Lambda term) => Sym_Show (BetaT term)
 
 -- Typing
+instance NameTyOf Show where
+	nameTyOf _c = ["Show"] `Mod` "Show"
 instance FixityOf Show
 instance ClassInstancesFor Show
 instance TypeInstancesFor Show
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Show
-instance (Source src, Inj_Sym ss Show) => ModuleFor src ss Show where
+instance (Source src, SymInj ss Show) => ModuleFor src ss Show where
 	moduleFor = ["Show"] `moduleWhere`
 	 [ "showsPrec" := teShow_showsPrec
 	 , "show"      := teShow_show
@@ -62,7 +64,7 @@
 tyShow :: Source src => Type src vs a -> Type src vs (Show a)
 tyShow a = tyConstLen @(K Show) @Show (lenVars a) `tyApp` a
 
-tyShowS :: Source src => Inj_Len vs => Type src vs ShowS
+tyShowS :: Source src => LenInj vs => Type src vs ShowS
 tyShowS = tyString ~> tyString
 
 -- ** 'Term's
diff --git a/Language/Symantic/Lib/Text.hs b/Language/Symantic/Lib/Text.hs
--- a/Language/Symantic/Lib/Text.hs
+++ b/Language/Symantic/Lib/Text.hs
@@ -14,7 +14,7 @@
 import Language.Symantic.Lib.MonoFunctor (Element)
 
 -- * Class 'Sym_Text'
-type instance Sym (Proxy Text) = Sym_Text
+type instance Sym Text = Sym_Text
 class Sym_Text term where
 	text :: Text -> term Text
 	default text :: Sym_Text (UnT term) => Trans term => Text -> term Text
@@ -33,6 +33,8 @@
 instance (Sym_Text term, Sym_Lambda term) => Sym_Text (BetaT term)
 
 -- Typing
+instance NameTyOf Text where
+	nameTyOf _c = ["Text"] `Mod` "Text"
 instance ClassInstancesFor Text where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
 	 | Just HRefl <- proj_ConstKiTy @_ @Text c
@@ -59,9 +61,9 @@
 instance ModuleFor src ss Text
 
 -- ** 'Type's
-tyText :: Source src => Inj_Len vs => Type src vs Text
+tyText :: Source src => LenInj vs => Type src vs Text
 tyText = tyConst @(K Text) @Text
 
 -- ** 'Term's
-teText :: Source src => Inj_Sym ss Text => Text -> Term src ss ts '[] (() #> Text)
+teText :: Source src => SymInj ss Text => Text -> Term src ss ts '[] (() #> Text)
 teText t = Term noConstraint tyText $ teSym @Text $ text t
diff --git a/Language/Symantic/Lib/Traversable.hs b/Language/Symantic/Lib/Traversable.hs
--- a/Language/Symantic/Lib/Traversable.hs
+++ b/Language/Symantic/Lib/Traversable.hs
@@ -13,7 +13,7 @@
 import Language.Symantic.Lib.Functor (f2)
 
 -- * Class 'Sym_Traversable'
-type instance Sym (Proxy Traversable) = Sym_Traversable
+type instance Sym Traversable = Sym_Traversable
 class Sym_Traversable term where
 	traverse :: Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))
 	default traverse :: Sym_Traversable (UnT term) => Trans term => Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))
@@ -31,13 +31,15 @@
 instance (Sym_Traversable term, Sym_Lambda term) => Sym_Traversable (BetaT term)
 
 -- Typing
+instance NameTyOf Traversable where
+	nameTyOf _c = ["Traversable"] `Mod` "Traversable"
 instance FixityOf Traversable
 instance ClassInstancesFor Traversable
 instance TypeInstancesFor Traversable
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g Traversable
-instance (Source src, Inj_Sym ss Traversable) => ModuleFor src ss Traversable where
+instance (Source src, SymInj ss Traversable) => ModuleFor src ss Traversable where
 	moduleFor = ["Traversable"] `moduleWhere`
 	 [ "traverse" := teTraversable_traverse
 	 ]
@@ -50,5 +52,5 @@
 teTraversable_traverse :: TermDef Traversable '[Proxy a, Proxy b, Proxy f, Proxy t] (Traversable t # Applicative f #> ((a -> f b) -> t a -> f (t b)))
 teTraversable_traverse = Term (tyTraversable t # tyApplicative f2) ((a0 ~> f2 `tyApp` b1) ~> t `tyApp` a0 ~> f2 `tyApp` (t `tyApp` b1)) $ teSym @Traversable $ lam2 traverse
 	where
-	t :: Source src => Inj_Len vs => Inj_Kind (K t) => Type src (Proxy a ': Proxy b ': Proxy c ': Proxy t ': vs) t
+	t :: Source src => LenInj vs => KindInj (K t) => Type src (Proxy a ': Proxy b ': Proxy c ': Proxy t ': vs) t
 	t = tyVar "t" $ VarS $ VarS $ VarS varZ
diff --git a/Language/Symantic/Lib/Tuple2.hs b/Language/Symantic/Lib/Tuple2.hs
--- a/Language/Symantic/Lib/Tuple2.hs
+++ b/Language/Symantic/Lib/Tuple2.hs
@@ -15,7 +15,7 @@
 import Language.Symantic.Lib.Monoid (tyMonoid)
 
 -- * Class 'Sym_Tuple2'
-type instance Sym (Proxy (,)) = Sym_Tuple2
+type instance Sym (,) = Sym_Tuple2
 class Sym_Tuple2 term where
 	tuple2 :: term a -> term b -> term (a, b)
 	fst :: term (a, b) -> term a
@@ -50,6 +50,8 @@
 instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term)
 
 -- Typing
+instance NameTyOf (,) where
+	nameTyOf _c = ["Tuple2"] `Mod` ","
 instance FixityOf (,) where
 	fixityOf _c = Just $ Fixity2 $ infixN (-1)
 instance ClassInstancesFor (,) where
@@ -100,30 +102,30 @@
  , Gram_Rule g
  , Gram_Comment g
  , Gram_Term src ss g
- , Inj_Sym ss (,)
+ , SymInj ss (,)
  ) => Gram_Term_AtomsFor src ss g (,) where
 	g_term_atomsFor =
 	 -- TODO: proper TupleSections
 	 [ rule "teTuple2_2" $
-		g_source $ parens $
+		source $ parens $
 		(\a b src ->
 			BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) a) b)
 		 <$> g_term
 		 <*  symbol ","
 		 <*> g_term
 	 , rule "teTuple2" $
-		g_source $
+		source $
 		(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2)
 		 <$ symbol "(,)"
 	 ]
-instance (Source src, Inj_Sym ss (,)) => ModuleFor src ss (,) where
+instance (Source src, SymInj ss (,)) => ModuleFor src ss (,) where
 	moduleFor = ["Tuple2"] `moduleWhere`
 	 [ "fst" := teTuple2_fst
 	 , "snd" := teTuple2_snd
 	 ]
 
 -- ** 'Term's
-tyTuple2 :: Source src => Inj_Len vs => Type src vs a -> Type src vs b -> Type src vs (a, b)
+tyTuple2 :: Source src => LenInj vs => Type src vs a -> Type src vs b -> Type src vs (a, b)
 tyTuple2 a b = tyConst @(K (,)) @(,) `tyApp` a `tyApp` b
 
 teTuple2 :: TermDef (,) '[Proxy a, Proxy b] (() #> (a -> b -> (a, b)))
diff --git a/Language/Symantic/Lib/Unit.hs b/Language/Symantic/Lib/Unit.hs
--- a/Language/Symantic/Lib/Unit.hs
+++ b/Language/Symantic/Lib/Unit.hs
@@ -9,7 +9,7 @@
 import Language.Symantic.Grammar
 
 -- * Class 'Sym_Unit'
-type instance Sym (Proxy ()) = Sym_Unit
+type instance Sym () = Sym_Unit
 class Sym_Unit term where
 	unit :: term ()
 	default unit :: Sym_Unit (UnT term) => Trans term => term ()
@@ -27,6 +27,8 @@
 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
 
 -- Typing
+instance NameTyOf () where
+	nameTyOf _c = [] `Mod` ""
 instance ClassInstancesFor () where
 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
 	 | Just HRefl <- proj_ConstKiTy @_ @() z
@@ -46,11 +48,11 @@
  ( Gram_Source src g
  , Gram_Rule g
  , Gram_Comment g
- , Inj_Sym ss ()
+ , SymInj ss ()
  ) => Gram_Term_AtomsFor src ss g () where
 	g_term_atomsFor =
 	 [ rule "teUnit" $
-		g_source $
+		source $
 		(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)
 		 <$ symbol "("
 		 <* symbol ")"
@@ -58,7 +60,7 @@
 instance ModuleFor src ss ()
 
 -- ** 'Type's
-tyUnit :: Source src => Inj_Len vs => Type src vs ()
+tyUnit :: Source src => LenInj vs => Type src vs ()
 tyUnit = tyConst @(K ()) @()
 
 -- ** 'Term's
diff --git a/Language/Symantic/Typing/Test.hs b/Language/Symantic/Typing/Test.hs
--- a/Language/Symantic/Typing/Test.hs
+++ b/Language/Symantic/Typing/Test.hs
@@ -70,13 +70,16 @@
  ]
 type SRC = SrcTe (NonEmpty P.SourcePos) SS
 
-cs :: Source src => Name2Type src
-cs =
-	Map.insert "String"
+impsTy :: Imports NameTy
+impsTy = importTypes @SS []
+
+modsTy :: Source src => ModulesTy src
+modsTy =
+	Map.insert ([] `Mod` "String")
 	 (TypeTLen $ \len -> TypeT $
 		tyConstLen @(K [])   @[]   len `tyApp`
 		tyConstLen @(K Char) @Char len) $
-	inj_Name2Type @SS
+	modulesTyInj @SS
 
 tests :: TestTree
 tests = testGroup "Typing" $
@@ -86,7 +89,7 @@
 		where
 		got :: Either (P.ParseError Char P.Dec)
 		              (Either (Error_Type SRC) (TypeVT SRC))
-		got = readType cs <$> P.runParser (unCF g) "" inp
+		got = readType impsTy modsTy <$> P.runParser (unCF g) "" inp
 		g :: Gram_Type SRC g => CF g (AST_Type SRC)
 		g = g_type <* eoi in
 	let (==>) = run; infixr 0 ==> in
@@ -142,7 +145,7 @@
 		let run inp = testCase inp $ got @?= Right (Left ())
 			where
 			got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))
-			got = left (Fun.const ()) . readType cs <$> P.runParser (unCF g) "" inp
+			got = left (Fun.const ()) . readType impsTy modsTy <$> P.runParser (unCF g) "" inp
 			g :: Gram_Type SRC g => CF g (AST_Type SRC)
 			g = g_type <* eoi in
 		run <$>
@@ -154,8 +157,10 @@
 		 , "Monad Eq"
 		 ]
  , testGroup "proveConstraint" $
-	let (==>) (typ::Type SRC '[] (t::Constraint)) expected =
-		testCase (show typ) $
+	let (==>) (typ::Type SRC SS (t::Constraint)) expected =
+		let imps = importTypes @SS [] in
+		let conf = config_Doc_Type{config_Doc_Type_imports = imps} in
+		testCase (showType conf typ) $
 		isJust (proveConstraint typ) @?= expected in
 	 [ tyEq          tyBool                      ==> True
 	 , tyOrd         tyBool                      ==> True
diff --git a/symantic-lib.cabal b/symantic-lib.cabal
--- a/symantic-lib.cabal
+++ b/symantic-lib.cabal
@@ -19,7 +19,7 @@
 -- PVP:  +-+------- breaking API changes
 --       | | +----- non-breaking API additions
 --       | | | +--- code changes with no API change
-version: 0.0.2.20170623
+version: 0.0.2.20170702
 
 Source-Repository head
   location: git://git.autogeree.net/symantic