diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,18 @@
 
 # CHANGELOG
 
+## 2.2.0
+### Removed
+* Module `Data.HSet.TypeLevel` removed
+
+### Changed
+* added dependency on `type-fun`
+* code rewritten with use of `type-fun` instead of `TypeLevel`
+* type class `SubHSet` simplified for constraint solver happiness
+
+### Added
+* `AllHGettable` typefamily for convenience
+
 ## 2.1.0
 ### Changed
 * `hgetTagged` moved to module `Data.HSet.Get`
diff --git a/hset.cabal b/hset.cabal
--- a/hset.cabal
+++ b/hset.cabal
@@ -1,5 +1,5 @@
 name:                hset
-version:             2.1.0
+version:             2.2.0
 synopsis:            Primitive list with elements of unique types.
 license:             BSD3
 license-file:        LICENSE
@@ -27,13 +27,13 @@
                      , Data.HSet.Reverse
                      , Data.HSet.SubHSet
                      , Data.HSet.Type
-                     , Data.HSet.TypeLevel
                      , Data.HSet.Union
 
 
   build-depends:       base >=4.7 && < 5
                      , deepseq
                      , tagged
+                     , type-fun
 
   default-extensions: CPP
                     , ConstraintKinds
diff --git a/src/Data/HSet/Get.hs b/src/Data/HSet/Get.hs
--- a/src/Data/HSet/Get.hs
+++ b/src/Data/HSet/Get.hs
@@ -1,17 +1,23 @@
 module Data.HSet.Get
        ( HGet(..)
        , HGettable
+       , AllHGettable
        , hgetTagged
        ) where
 
 import Data.HSet.Type
-import Data.HSet.TypeLevel
 import Data.Tagged
+import GHC.Exts
+import TypeFun.Data.List
+import TypeFun.Data.Peano
 
 #if !(MIN_VERSION_base(4, 8, 0))
 import Control.Applicative
 #endif
 
+{-$setup
+>>> import Data.Proxy
+-}
 
 {- | Heterogeneous read arbitrarily element from hset
 
@@ -31,20 +37,25 @@
 
 -}
 
-class (i ~ (Index e els)) => HGet els e i | els i -> e where
+class (i ~ (IndexOf e els)) => HGet els e i | els i -> e where
   -- | Gets any data from HSet for you
   hget :: HSet els -> e
 
 instance HGet (e ': els) e 'Z where
   hget (HSCons e _) = e
 
-instance (('S i) ~ (Index e (e1 ': els)), HGet els e i)
+instance (('S i) ~ (IndexOf e (e1 ': els)), HGet els e i)
          => HGet (e1 ': els) e ('S i) where
   hget (HSCons _ els) = hget els
 
 -- | Enables deriving of the fact that 'e' is contained within 'els' and it's
 -- safe to say that 'hget' can be performed on this particular pair.
-type HGettable els e = HGet els e (Index e els)
+type HGettable els e = HGet els e (IndexOf e els)
+
+-- | Reduces to __(HGettable els e1, HGettable els e2, ..)__
+type family AllHGettable (els :: [k]) (subels :: [k]) :: Constraint where
+  AllHGettable els '[] = ()
+  AllHGettable els (e ': subels) = (HGettable els e, AllHGettable els subels)
 
 
 {- |
diff --git a/src/Data/HSet/Modify.hs b/src/Data/HSet/Modify.hs
--- a/src/Data/HSet/Modify.hs
+++ b/src/Data/HSet/Modify.hs
@@ -10,32 +10,33 @@
        ) where
 
 import Data.HSet.Type
-import Data.HSet.TypeLevel
 import Data.Tagged
+import TypeFun.Data.List
+import TypeFun.Data.Peano
 
 #if !(MIN_VERSION_base(4, 8, 0))
 import Control.Applicative
 #endif
 
-class (i ~ (Index e1 els1), i ~ (Index e2 els2))
+class (i ~ (IndexOf e1 els1), i ~ (IndexOf e2 els2))
       => HModify els1 els2 e1 e2 i
-       | els1 i     -> e1  , els2 i     -> e2
-       , els1 e1 e2 i -> els2, els2 e1 e2 i -> els1 where
+       | els1 els2 e2 i -> e1  , els1 els2 e1 i -> e2
+       , els1 e1 e2 i   -> els2, els2 e1 e2 i   -> els1 where
   hmodify :: (e1 -> e2) -> HSet els1 -> HSet els2
 
-instance ('False ~ Elem e2 els)
+instance (NotElem e2 els)
          => HModify (e1 ': els) (e2 ': els) e1 e2 'Z where
   hmodify f (HSCons e els) = HSCons (f e) els
 
-instance ( ('S i) ~ (Index e1 (ex ': els1))
-         , ('S i) ~ (Index e2 (ex ': els2))
+instance ( ('S i) ~ (IndexOf e1 (ex ': els1))
+         , ('S i) ~ (IndexOf e2 (ex ': els2))
          , HModify els1 els2 e1 e2 i
-         , 'False ~ (Elem ex els2) )
+         , NotElem ex els2 )
          => HModify (ex ': els1) (ex ': els2) e1 e2 ('S i) where
   hmodify f (HSCons e els) = HSCons e $ hmodify f els
 
 -- | Check that we can turn one hset to another
-type HModifiable els1 els2 e1 e2 = HModify els1 els2 e1 e2 (Index e1 els1)
+type HModifiable els1 els2 e1 e2 = HModify els1 els2 e1 e2 (IndexOf e1 els1)
 
 -- | Helper type infering that hset 'els' contains element of type 'e'
 -- and can be modified
diff --git a/src/Data/HSet/Remove.hs b/src/Data/HSet/Remove.hs
--- a/src/Data/HSet/Remove.hs
+++ b/src/Data/HSet/Remove.hs
@@ -5,8 +5,9 @@
        ) where
 
 import Data.HSet.Type
-import Data.HSet.TypeLevel
 import Data.Typeable
+import TypeFun.Data.List
+import TypeFun.Data.Peano
 
 #if !(MIN_VERSION_base(4, 8, 0))
 import Control.Applicative
@@ -16,12 +17,12 @@
 -- | Remove i's element from hset. Second argument is a resulting hset
 -- type
 class HRemove els1 els2 i | els1 i -> els2 where
-  hremove :: Proxy i -> HSet els1 -> HSet els2
+  hremove :: forall proxy. proxy i -> HSet els1 -> HSet els2
 
 instance HRemove (e ': els) els 'Z where
   hremove _ (HSCons _ els) = els
 
-instance ( 'False ~ (Elem e els2)
+instance ( NotElem e els2
          , HRemove els1 els2 i )
          => HRemove (e ': els1) (e ': els2) ('S i) where
   hremove _ (HSCons e els) = HSCons e $ hremove (Proxy :: Proxy i) els
@@ -40,7 +41,7 @@
 
 -- | Constraints that e can be removed from els1 and els2 will be
 -- produced in result
-type HDeletable e els1 els2 = HRemove els1 els2 (Index e els1)
+type HDeletable e els1 els2 = HRemove els1 els2 (IndexOf e els1)
 
 -- | Delete specific element from els1 and returns HSet with els2
 hdelete :: forall proxy els1 els2 e
@@ -48,4 +49,4 @@
         => proxy e
         -> HSet els1
         -> HSet els2
-hdelete _ h = hremove (Proxy :: Proxy (Index e els1)) h
+hdelete _ h = hremove (Proxy :: Proxy (IndexOf e els1)) h
diff --git a/src/Data/HSet/Reverse.hs b/src/Data/HSet/Reverse.hs
--- a/src/Data/HSet/Reverse.hs
+++ b/src/Data/HSet/Reverse.hs
@@ -5,7 +5,7 @@
        ) where
 
 import Data.HSet.Type
-import Data.HSet.TypeLevel
+import TypeFun.Data.List
 
 -- | This is auxiliary typeclass for inversing the order of hset
 -- elements
@@ -16,13 +16,12 @@
 instance HReverse acc '[] acc where
   hreverse' acc _ = acc
 
-instance ( 'False ~ (Elem e (ah ': at))
+instance ( NotElem e (ah ': at)
          , HReverse (e ': ah ': at) els1 els2 )
          => HReverse (ah ': at) (e ': els1) els2 where
   hreverse' acc (HSCons e els1) = hreverse' (HSCons e acc) els1
 
-instance ( (e ': els1) ~ Reverse els2 -- Little trick to help inference of els1 from els2
-         , HReverse '[e] els1 els2 )
+instance (HReverse '[e] els1 els2)
          => HReverse '[] (e ': els1) els2 where
   hreverse' acc (HSCons e els1) = hreverse' (HSCons e acc) els1
 
diff --git a/src/Data/HSet/SubHSet.hs b/src/Data/HSet/SubHSet.hs
--- a/src/Data/HSet/SubHSet.hs
+++ b/src/Data/HSet/SubHSet.hs
@@ -6,7 +6,7 @@
 
 import Data.HSet.Get
 import Data.HSet.Type
-import Data.HSet.TypeLevel
+import TypeFun.Data.List
 
 #if !(MIN_VERSION_base(4, 8, 0))
 import Control.Applicative
@@ -33,27 +33,18 @@
 
 -}
 
-class (eq ~ TEq els els2)
-      => SubHSet els els2 eq where
+class SubHSet els els2 where
   subHSet :: HSet els -> HSet els2
 
-instance (eq ~ TEq els '[]) => SubHSet els '[] eq where
+instance SubHSet els '[] where
   subHSet _ = HSNil
 
-instance ( HGettable els el, 'False ~ Elem el els2
-         , SubHSet els els2 subeq
-         , 'False ~ TEq els (el ': els2) )
-         => SubHSet els (el ': els2) 'False where
+instance ( HGettable els el, NotElem el els2
+         , SubHSet els els2 )
+         => SubHSet els (el ': els2) where
   subHSet h = HSCons (hget h :: el) (subHSet h :: HSet els2)
 
-instance ( HGettable els el, 'False ~ Elem el els2
-         , SubHSet els els2 subeq
-         , els ~ (el ': els2)
-         , 'True ~ TEq els (el ': els2) )
-         => SubHSet els (el ': els2) 'True where
-  subHSet h = h
-
-type SubHSettable els1 els2 = (SubHSet els1 els2 (TEq els1 els2))
+type SubHSettable = SubHSet
 
 {- | Like 'subHSet' but with proxy for convenience
 
diff --git a/src/Data/HSet/Type.hs b/src/Data/HSet/Type.hs
--- a/src/Data/HSet/Type.hs
+++ b/src/Data/HSet/Type.hs
@@ -1,8 +1,8 @@
 module Data.HSet.Type where
 
-import Data.HSet.TypeLevel
-import Data.Typeable
 import Control.DeepSeq
+import Data.Typeable
+import TypeFun.Data.List
 
 #if !(MIN_VERSION_base(4, 8, 0))
 import Control.Applicative
@@ -16,7 +16,7 @@
 
 data HSet (elems :: [*]) where
   HSNil  :: HSet '[]
-  HSCons :: ('False ~ (Elem elem elems)) => !elem -> HSet elems -> HSet (elem ': elems)
+  HSCons :: (NotElem elem elems) => !elem -> HSet elems -> HSet (elem ': elems)
   deriving ( Typeable )
 
 instance Show (HSet '[]) where
diff --git a/src/Data/HSet/TypeLevel.hs b/src/Data/HSet/TypeLevel.hs
deleted file mode 100644
--- a/src/Data/HSet/TypeLevel.hs
+++ /dev/null
@@ -1,119 +0,0 @@
-module Data.HSet.TypeLevel
-       ( Nat(..)
-       , Elem
-       , Index
-       , MayIndexGo
-       , MayIndex
-       , MayFstIndexSnd
-       , TEq
-       , Length
-       , Append
-       , AppendUniq
-       , Union
-       , UnionList'
-       , UnionList
-       , XReverse
-       , Reverse
-       , Delete
-       , Replace
-       , TagElem
-       , And
-       , HSubset
-       ) where
-
-import Data.Tagged
-
-data Nat = Z | S Nat
-
--- | Calculates to 'True if first type argument contained in second
--- list element
-type family Elem (typ :: k) (typs :: [k]) :: Bool where
-    Elem typ '[]             = 'False
-    Elem typ (typ ': typs)   = 'True
-    Elem typ1 (typ2 ': typs) = Elem typ1 typs
-
--- | Calculates to Nat kinded type describing the index of first
--- argument in second argument
-type family Index (typ :: k) (typs :: [k]) :: Nat where
-  Index t (t ': ts) = 'Z
-  Index t (tt ': ts) = 'S (Index t ts)
-
-
-type family MayIndexGo (typ :: k) (typs :: [k]) (acc :: Nat) :: (Maybe Nat) where
-  MayIndexGo t (t ': ts)  acc = 'Just acc
-  MayIndexGo t (tt ': ts) acc = MayIndexGo t ts ('S acc)
-  MayIndexGo t '[]        acc = 'Nothing
-
-type MayIndex typ typs = MayIndexGo typ typs 'Z
-
-
-type family MayFstIndexSnd (ts1 :: [k]) (ts2 :: [k]) :: (Maybe Nat) where
-  MayFstIndexSnd (e ': els) x = MayIndex e x
-  MayFstIndexSnd '[] x        = 'Nothing
-
-type family TEq (t1 :: k) (t2 :: k) :: Bool where
-  TEq a a = 'True
-  TEq a b = 'False
-
--- | Type level list length
-type family Length (list :: [*]) :: Nat where
-  Length '[] = 'Z
-  Length (x ': xs) = 'S (Length xs)
-
-type family Append (l1 :: [*]) (l2 :: [*]) :: [*] where
-  Append '[] x = x
-  Append x '[] = x
-  Append (x ': xs) ys = x ': (Append xs ys)
-
--- | Append element to type list if element is not presented in list
--- already
-type family AppendUniq (typs :: [*]) (typ :: *) :: [*] where
-  AppendUniq (t ': ts) t = t ': ts
-  AppendUniq (t ': ts) t1 = t ': (AppendUniq ts t1)
-  AppendUniq '[] t1 = '[t1]
-
--- | Calculates union two lists
-type family Union (l1 :: [*]) (l2 :: [*]) :: [*] where
-  Union l1 '[] = l1
-  Union l1 (l ': ls) = Union (AppendUniq l1 l) ls
-
-type family UnionList' (acc :: [*]) (ls :: [[*]]) :: [*] where
-  UnionList' acc (e ': es) = UnionList' (Union acc e) es
-  UnionList' acc '[] = acc
-
--- | Union list of lists of elements. Return just unique elements of
--- each nested list
-type UnionList l = UnionList' '[] l
-
-type family XReverse (acc :: [*]) (l :: [*]) :: [*] where
-  XReverse acc '[] = acc
-  XReverse acc (e ': els) = XReverse (e ': acc) els
-
--- | Reverse list of elements
-type Reverse a = XReverse '[] a
-
--- | Delete element from type list
-type family Delete (typ :: *) (typs :: [*]) :: [*] where
-  Delete x '[] = '[]
-  Delete x (x ': ys) = Delete x ys
-  Delete x (y ': ys) = y ': (Delete x ys)
-
--- | Replace first arbitrary element 'typ1' in type list with 'typ2'
-type family Replace (typ1 :: *) (typ2 :: *) (typs :: [*]) :: [*] where
-  Replace a b (a ': xs) = (b ': xs)
-  Replace a b (x ': xs) = x ': (Replace a b xs)
-
--- | Wrap first element with __Tagged tag__
-type TagElem (tag :: k) (typ :: *) (typs :: [*])
-  = Replace typ (Tagged tag typ) typs
-
-type family And (a :: Bool) (b :: Bool) where
-  And 'False x      = 'False
-  And x      'False = 'False
-  And x      y      = 'True
-
--- | Checks if the former subset included in the latter one.
-type family HSubset (h1 :: [k]) (h2 :: [k]) where
-  HSubset '[]         x   = 'True
-  HSubset x           '[] = 'False
-  HSubset (h1 ': tl2) h2  = And (Elem h1 h2) (HSubset tl2 h2)
diff --git a/src/Data/HSet/Union.hs b/src/Data/HSet/Union.hs
--- a/src/Data/HSet/Union.hs
+++ b/src/Data/HSet/Union.hs
@@ -2,13 +2,18 @@
 
 import Data.HSet.Remove
 import Data.HSet.Type
-import Data.HSet.TypeLevel
 import Data.Typeable
+import TypeFun.Data.List
+import TypeFun.Data.Peano
 
 #if !(MIN_VERSION_base(4, 8, 0))
 import Control.Applicative
 #endif
 
+type family MayFstIndexSnd (ts1 :: [k]) (ts2 :: [k]) :: (Maybe N) where
+  MayFstIndexSnd (e ': els) x = IndexOfMay e x
+  MayFstIndexSnd '[]        x = 'Nothing
+
 class ( fidx ~ (MayFstIndexSnd els1 els2)
       , sidx ~ (MayFstIndexSnd els2 els1) )
       => HUnion els1 els2 elsr fidx sidx
@@ -25,21 +30,21 @@
   hunion a _ = a
 
 instance ( HUnionable els1 els2 elsr
-         , 'False ~ (Elem e1 (e2 ': elsr))
-         , 'False ~ (Elem e2 elsr)
+         , NotElem e1 (e2 ': elsr)
+         , NotElem e2 elsr
          , 'Nothing ~ (MayFstIndexSnd (e1 ': els1) (e2 ': els2))
          , 'Nothing ~ (MayFstIndexSnd (e2 ': els2) (e1 ': els1)) )
          => HUnion (e1 ': els1) (e2 ': els2) (e1 ': e2 ': elsr) 'Nothing 'Nothing where
   hunion (HSCons e1 els1) (HSCons e2 els2) = HSCons e1 $ HSCons e2 $ hunion els1 els2
 
 instance ( HUnionable els1 els2 elsr
-         , 'False ~ (Elem e elsr) )
+         , NotElem e elsr )
          => HUnion (e ': els1) (e ': els2) (e ': elsr) ('Just 'Z) ('Just 'Z) where
   hunion (HSCons e els1) (HSCons _ els2) = HSCons e $ hunion els1 els2
 
 instance ( HRemove els2 elsx fi
          , HUnionable els1 elsx elsr
-         , 'False ~ (Elem e1 elsr)
+         , NotElem e1 elsr
          , ('Just ('S fi)) ~ (MayFstIndexSnd (e1 ': els1) (e2 ': els2))
          , ('Just si) ~ (MayFstIndexSnd (e2 ': els2) (e1 ': els1)) )
          => HUnion (e1 ': els1) (e2 ': els2) (e1 ': elsr) ('Just ('S fi)) ('Just si) where
@@ -47,14 +52,14 @@
 
 instance ( HRemove els2 elsx fi
          , HUnionable els1 elsx elsr
-         , 'False ~ (Elem e1 elsr)
+         , NotElem e1 elsr
          , ('Just fi) ~ (MayFstIndexSnd (e1 ': els1) els2)
          , 'Nothing ~ (MayFstIndexSnd els2 (e1 ': els1)) )
          => HUnion (e1 ': els1) els2 (e1 ': elsr) ('Just fi) 'Nothing where
   hunion (HSCons e1 els1) els2 = HSCons e1 $ hunion els1 $ hremove (Proxy :: Proxy fi) els2
 
 instance ( HUnionable els1 els2 elsr
-         , 'False ~ (Elem e1 elsr)
+         , NotElem e1 elsr
          , 'Nothing ~ (MayFstIndexSnd (e1 ': els1) (e2 ': els2))
          , ('Just si) ~ (MayFstIndexSnd (e2 ': els2) (e1 ': els1)) )
          => HUnion (e1 ': els1) (e2 ': els2) (e1 ': elsr) 'Nothing ('Just si) where