diff --git a/kind-apply.cabal b/kind-apply.cabal
--- a/kind-apply.cabal
+++ b/kind-apply.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                kind-apply
-version:             0.2.0.0
+version:             0.3.0.0
 synopsis:            Utilities to work with lists of types
 description:         This packages reifies the concept of list of types, and application of those to list constructors.
 -- bug-reports:
diff --git a/src/Data/PolyKinded.hs b/src/Data/PolyKinded.hs
--- a/src/Data/PolyKinded.hs
+++ b/src/Data/PolyKinded.hs
@@ -13,7 +13,7 @@
 {-# language ConstraintKinds        #-}
 module Data.PolyKinded (
   -- * Lists of types and application
-  LoT(..), (:@@:)
+  LoT(..), (:@@:), LoT1, LoT2
   -- * Splitting types
 , SplitF, Nat(..), TyEnv(..), SplitN
 ) where
@@ -26,6 +26,9 @@
   LoT0    ::                LoT (*)
   -- | Cons a type with a list of types.
   (:&&:)  :: k -> LoT ks -> LoT (k -> ks)
+
+type LoT1 a = a ':&&: 'LoT0
+type LoT2 a b = a ':&&: b ':&&: LoT0
 
 -- | Apply a list of types to a type constructor.
 --
diff --git a/src/Data/PolyKinded/Atom.hs b/src/Data/PolyKinded/Atom.hs
--- a/src/Data/PolyKinded/Atom.hs
+++ b/src/Data/PolyKinded/Atom.hs
@@ -4,43 +4,74 @@
 {-# language DataKinds       #-}
 {-# language PolyKinds       #-}
 {-# language ConstraintKinds #-}
+{-# language RankNTypes      #-}
+{-# language AllowAmbiguousTypes  #-}
+{-# language UndecidableInstances #-}
 module Data.PolyKinded.Atom where
 
 import Data.Kind
 import Data.PolyKinded
+import Data.Type.Equality
+import GHC.Exts
 
-data TyVar d k where
+data TyVar (d :: *) (k :: TYPE r) where
   VZ :: TyVar (x -> xs) x
   VS :: TyVar xs k -> TyVar (x -> xs) k
 
-type V0 = 'Var 'VZ
-type V1 = 'Var ('VS 'VZ)
-type V2 = 'Var ('VS ('VS 'VZ))
-type V3 = 'Var ('VS ('VS ('VS 'VZ)))
-type V4 = 'Var ('VS ('VS ('VS ('VS 'VZ))))
-type V5 = 'Var ('VS ('VS ('VS ('VS ('VS 'VZ)))))
-type V6 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))
-type V7 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))
-type V8 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))))
-type V9 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))))
+type Var0 = 'Var 'VZ
+type Var1 = 'Var ('VS 'VZ)
+type Var2 = 'Var ('VS ('VS 'VZ))
+type Var3 = 'Var ('VS ('VS ('VS 'VZ)))
+type Var4 = 'Var ('VS ('VS ('VS ('VS 'VZ))))
+type Var5 = 'Var ('VS ('VS ('VS ('VS ('VS 'VZ)))))
+type Var6 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))
+type Var7 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))
+type Var8 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))))
+type Var9 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))))
 
 infixr 5 :&:
-data Atom d k where
-  Var   :: TyVar d k -> Atom d k
-  Kon   :: k         -> Atom d k
+infixr 5 :=>>:
+data Atom (d :: *) (k :: TYPE r) where
+  Var :: TyVar d k -> Atom d k
+  Kon :: k         -> Atom d k
   (:@:) :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2
   (:&:) :: Atom d Constraint -> Atom d Constraint -> Atom d Constraint
+  ForAll  :: Atom (d1 -> d) (*) -> Atom d (*)
+  (:=>>:) :: Atom d Constraint -> Atom d (*) -> Atom d (*)
 
-type f :$: x = 'Kon f ':@: x
-type a :~: b = 'Kon (~) ':@: a ':@: b
+type f :$:  x = 'Kon f ':@: x
+type a :~:  b = 'Kon (~) ':@: a ':@: b
+type a :~~: b = 'Kon (~~) ':@: a ':@: b
 
-type family Ty (t :: Atom d k) (tys :: LoT d) :: k where
-  Ty ('Var 'VZ)     (t ':&&: ts) = t
-  Ty ('Var ('VS v)) (t ':&&: ts) = Ty ('Var v) ts
-  Ty ('Kon t)       tys          = t
-  Ty (f ':@: x)     tys          = (Ty f tys) (Ty x tys)
-  Ty (c ':&: d)     tys          = (Ty c tys, Ty d tys)
+type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
+  Interpret ('Var 'VZ)     (t ':&&: ts) = t
+  Interpret ('Var ('VS v)) (t ':&&: ts) = Interpret ('Var v) ts
+  Interpret ('Kon t)       tys = t
+  Interpret (f ':@: x)     tys = (Interpret f tys) (Interpret x tys)
+  Interpret (c ':&: d)     tys = (Interpret c tys, Interpret d tys)
+  Interpret (ForAll f)     tys = ForAllI f tys
+  Interpret (c ':=>>: f)   tys = SuchThatI c f tys
 
+newtype ForAllI (f :: Atom (d1 -> d) (*)) (tys :: LoT d) where
+  ForAllI :: (forall t. Interpret f (t ':&&: tys)) -> ForAllI f tys
+
+newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d (*)) (tys :: LoT d) where
+  SuchThatI :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys
+
 type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) :: Constraint where
   Satisfies '[]       tys = ()
-  Satisfies (c ': cs) tys = (Ty c tys, Satisfies cs tys)
+  Satisfies (c ': cs) tys = (Interpret c tys, Satisfies cs tys)
+
+type family ContainsTyVar (v :: TyVar d k) (t :: Atom d p) :: Bool where
+  ContainsTyVar v (Var v)     = 'True
+  ContainsTyVar v (Var w)     = 'False
+  ContainsTyVar v (Kon t)     = 'False
+  ContainsTyVar v (f :@: x)   = Or (ContainsTyVar v f) (ContainsTyVar v x)
+  ContainsTyVar v (x :&: y)   = Or (ContainsTyVar v x) (ContainsTyVar v y)
+  ContainsTyVar v (c :=>>: f) = Or (ContainsTyVar v c) (ContainsTyVar v f)
+  ContainsTyVar v (ForAll f)  = ContainsTyVar (VS v) f
+
+type family Or (x :: Bool) (y :: Bool) :: Bool where
+  Or True  thing = True
+  Or thing True  = True
+  Or False False = False