diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,10 @@
+0.3.1
+-----------------------------------------------------
+* Removed `Reifiable`
+* Now `library` yields desired dictionaries
+* Added `remember`
+* Added `strike` and `strikeAt`
+
 0.3
 -----------------------------------------------------
 * Renamed `generate` to `htabulate`
diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,5 +1,5 @@
 name:                extensible
-version:             0.3
+version:             0.3.1
 synopsis:            Extensible, efficient, lens-friendly data types
 homepage:            https://github.com/fumieval/extensible
 bug-reports:         http://github.com/fumieval/extensible/issues
@@ -50,7 +50,7 @@
     , FlexibleContexts
     , FlexibleInstances
     , PolyKinds
-  build-depends:       base >= 4.7 && <5, template-haskell, deepseq, binary < 1
+  build-depends:       base >= 4.7 && <5, template-haskell, binary < 1, constraints
   hs-source-dirs:      src
   ghc-options: -Wall -O2
   default-language:    Haskell2010
diff --git a/src/Data/Extensible.hs b/src/Data/Extensible.hs
--- a/src/Data/Extensible.hs
+++ b/src/Data/Extensible.hs
@@ -23,7 +23,8 @@
 -----------------------------------------------------------------------------
 module Data.Extensible (
   -- * Reexport
-  module Data.Extensible.Inclusion
+  module Data.Extensible.Dictionary
+  , module Data.Extensible.Inclusion
   , module Data.Extensible.League
   , module Data.Extensible.Match
   , module Data.Extensible.Plain
@@ -43,7 +44,7 @@
 import Data.Extensible.Union
 import Data.Extensible.Record
 import Data.Extensible.Internal.Rig
-import Data.Extensible.Dictionary ()
+import Data.Extensible.Dictionary
 
 -------------------------------------------------------------
 
diff --git a/src/Data/Extensible/Dictionary.hs b/src/Data/Extensible/Dictionary.hs
--- a/src/Data/Extensible/Dictionary.hs
+++ b/src/Data/Extensible/Dictionary.hs
@@ -19,39 +19,11 @@
 import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
 import qualified Data.Binary as B
-
--- | Reifiable classes
-class Reifiable c where
-  -- | The associated dictionary which subsumes essential methods.
-  data Dictionary c (h :: k -> *) (x :: k)
-
-  -- | Fetch the 'Dictionary'.
-  library :: WrapForall c h xs => Dictionary c h :* xs
-
-instance Reifiable Show where
-  data Dictionary Show h x = DictShow { getShowsPrec :: Int -> h x -> ShowS }
-  library :: forall h xs. WrapForall Show h xs => Dictionary Show h :* xs
-  library = htabulateFor (Proxy :: Proxy (Instance1 Show h)) $ const $ DictShow showsPrec
-
-instance Reifiable Eq where
-  data Dictionary Eq h x = DictEq { getEq :: h x -> h x -> Bool }
-  library :: forall h xs. WrapForall Eq h xs => Dictionary Eq h :* xs
-  library = htabulateFor (Proxy :: Proxy (Instance1 Eq h)) $ const $ DictEq (==)
-
-instance Reifiable Ord where
-  data Dictionary Ord h x = DictOrd { getCompare :: h x -> h x -> Ordering }
-  library :: forall h xs. WrapForall Ord h xs => Dictionary Ord h :* xs
-  library = htabulateFor (Proxy :: Proxy (Instance1 Ord h)) $ const $ DictOrd compare
-
-instance Reifiable Monoid where
-  data Dictionary Monoid h x = DictMonoid { getMempty :: h x, getMappend :: h x -> h x -> h x }
-  library :: forall h xs. WrapForall Monoid h xs => Dictionary Monoid h :* xs
-  library = htabulateFor (Proxy :: Proxy (Instance1 Monoid h)) $ const $ DictMonoid mempty mappend
+import Data.Constraint
 
-instance Reifiable B.Binary where
-  data Dictionary B.Binary h x = DictBinary { getGet :: B.Get (h x), getPut :: h x -> B.Put }
-  library :: forall h xs. WrapForall B.Binary h xs => Dictionary B.Binary h :* xs
-  library = htabulateFor (Proxy :: Proxy (Instance1 B.Binary h)) $ const $ DictBinary B.get B.put
+library :: forall c xs. Forall c xs => Comp Dict c :* xs
+library = htabulateFor (Proxy :: Proxy c) $ const (Comp Dict)
+{-# INLINE library #-}
 
 instance WrapForall Show h xs => Show (h :* xs) where
   showsPrec d = showParen (d > 0)
@@ -59,42 +31,42 @@
     . foldr (.) id
     . getMerged
     . hfoldMap getConst'
-    . hzipWith (\f h -> Const' $ MergeList [getShowsPrec f 0 h . showString " <: "]) library
+    . hzipWith (\(Comp Dict) h -> Const' $ MergeList [showsPrec 0 h . showString " <: "]) (library :: Comp Dict (Instance1 Show h) :* xs)
 
 instance WrapForall Eq h xs => Eq (h :* xs) where
   xs == ys = getAll $ hfoldMap (All . getConst')
-    $ hzipWith3 (\f x y -> Const' $ getEq f x y) library xs ys
+    $ hzipWith3 (\(Comp Dict) x y -> Const' $ x == y) (library :: Comp Dict (Instance1 Eq h) :* xs) xs ys
   {-# INLINE (==) #-}
 
 instance (Eq (h :* xs), WrapForall Ord h xs) => Ord (h :* xs) where
   compare xs ys = hfoldMap getConst'
-    $ hzipWith3 (\f x y -> Const' $ getCompare f x y) library xs ys
+    $ hzipWith3 (\(Comp Dict) x y -> Const' $ compare x y) (library :: Comp Dict (Instance1 Ord h) :* xs) xs ys
   {-# INLINE compare #-}
 
 instance WrapForall Monoid h xs => Monoid (h :* xs) where
-  mempty = hmap getMempty library
+  mempty = hmap (\(Comp Dict) -> mempty) (library :: Comp Dict (Instance1 Monoid h) :* xs)
   {-# INLINE mempty #-}
-  mappend xs ys = hzipWith3 getMappend library xs ys
+  mappend xs ys = hzipWith3 (\(Comp Dict) -> mappend) (library :: Comp Dict (Instance1 Monoid h) :* xs) xs ys
   {-# INLINE mappend #-}
 
 instance WrapForall B.Binary h xs => B.Binary (h :* xs) where
   get = hgenerateFor (Proxy :: Proxy (Instance1 B.Binary h)) (const B.get)
-  put = flip appEndo (return ()) . hfoldMap getConst' . hzipWith (\dic x -> Const' $ Endo $ (getPut dic x >>)) library
+  put = flip appEndo (return ()) . hfoldMap getConst' . hzipWith (\(Comp Dict) x -> Const' $ Endo $ (B.put x >>)) (library :: Comp Dict (Instance1 B.Binary h) :* xs)
 
 instance WrapForall Show h xs => Show (h :| xs) where
   showsPrec d (UnionAt pos h) = showParen (d > 10) $ showString "embed "
-    . views (sectorAt pos) getShowsPrec library 11 h
+    . views (sectorAt pos) (\(Comp Dict) -> showsPrec 11 h) (library :: Comp Dict (Instance1 Show h) :* xs)
 
 instance WrapForall Eq h xs => Eq (h :| xs) where
   UnionAt p g == UnionAt q h = case compareMembership p q of
     Left _ -> False
-    Right Refl -> views (sectorAt p) getEq library g h
+    Right Refl -> views (sectorAt p) (\(Comp Dict) -> g == h) (library :: Comp Dict (Instance1 Eq h) :* xs)
   {-# INLINE (==) #-}
 
 instance (Eq (h :| xs), WrapForall Ord h xs) => Ord (h :| xs) where
   UnionAt p g `compare` UnionAt q h = case compareMembership p q of
     Left x -> x
-    Right Refl -> views (sectorAt p) getCompare library g h
+    Right Refl -> views (sectorAt p) (\(Comp Dict) -> compare g h) (library :: Comp Dict (Instance1 Ord h) :* xs)
   {-# INLINE compare #-}
 
 -- | Forall upon a wrapper
diff --git a/src/Data/Extensible/Inclusion.hs b/src/Data/Extensible/Inclusion.hs
--- a/src/Data/Extensible/Inclusion.hs
+++ b/src/Data/Extensible/Inclusion.hs
@@ -16,6 +16,7 @@
   , runMembership
   , (∈)()
   , Member(..)
+  , remember
   , Expecting
   , Missing
   , Ambiguous
diff --git a/src/Data/Extensible/Internal.hs b/src/Data/Extensible/Internal.hs
--- a/src/Data/Extensible/Internal.hs
+++ b/src/Data/Extensible/Internal.hs
@@ -28,6 +28,7 @@
   , navR
   , (:*)(..)
   , Member(..)
+  , remember
   , (∈)()
   , Nat(..)
   , ToInt(..)
@@ -61,7 +62,6 @@
 import Unsafe.Coerce
 import Data.Typeable
 import Language.Haskell.TH hiding (Pred)
-import Control.DeepSeq
 import Data.Bits
 import Data.Word
 
@@ -79,6 +79,13 @@
 -- | The position of @x@ in the type level set @xs@.
 newtype Membership (xs :: [k]) (x :: k) = Membership { getMemberId :: Word } deriving Typeable
 
+newtype Remembrance xs x r = Remembrance (Member xs x => r)
+
+-- | Remember that @Member xs x@ from 'Membership'.
+remember :: forall xs x r. Membership xs x -> (Member xs x => r) -> r
+remember pos r = unsafeCoerce (Remembrance r :: Remembrance xs x r) pos
+{-# INLINE remember #-}
+
 -- | Lookup types
 type family ListIndex (n :: Nat) (xs :: [k]) :: k where
   ListIndex Zero (x ': xs) = x
@@ -96,7 +103,7 @@
   Div2 (DNat n) = n
   Div2 Zero = Zero
 
--- | The extensible product type
+-- | The type of extensible products.
 data (h :: k -> *) :* (s :: [k]) where
   Nil :: h :* '[]
   Tree :: !(h x)
@@ -123,9 +130,6 @@
   lookupTree _ f (Tree h a b) = fmap (\b' -> Tree h a b') (lookupTree (Proxy :: Proxy (Div2 (Pred (DNat n)))) (unsafeCoerce f) b)
   {-# INLINE lookupTree #-}
 
-instance NFData (Membership xs x) where
-  rnf (Membership a) = rnf a
-
 instance Show (Membership xs x) where
   show (Membership n) = "$(ord " ++ show n ++ ")"
 
@@ -141,7 +145,7 @@
 runMembership (Membership n) _ r = r (Membership (n - 1))
 {-# INLINE runMembership #-}
 
--- | PRIVILEGED: Compare two 'Membership's.
+-- | Compare two 'Membership's.
 compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
 compareMembership (Membership m) (Membership n) = case compare m n of
   EQ -> Right (unsafeCoerce Refl)
@@ -191,7 +195,7 @@
 type family Head (xs :: [k]) :: k where
   Head (x ': xs) = x
 
-class (LookupTree (Head (Lookup x xs)) xs x) => Member xs x where
+class Member xs x where
   membership :: Membership xs x
 
 -- | A type sugar to make type error more readable.
@@ -209,7 +213,7 @@
   Check x '[] = Missing x
   Check x xs = Ambiguous x
 
-instance (Check x (Lookup x xs) ~ Expecting one, ToInt one, LookupTree (Head (Lookup x xs)) xs x) => Member xs x where
+instance (Check x (Lookup x xs) ~ Expecting one, ToInt one) => Member xs x where
   membership = Membership (theInt (Proxy :: Proxy one))
   {-# INLINE membership #-}
 
diff --git a/src/Data/Extensible/Product.hs b/src/Data/Extensible/Product.hs
--- a/src/Data/Extensible/Product.hs
+++ b/src/Data/Extensible/Product.hs
@@ -161,8 +161,8 @@
 {-# INLINE hmapWithIndex #-}
 
 -- | /O(log n)/ A lens for a specific element.
-sector :: forall h x xs. (x ∈ xs) => Lens' (h :* xs) (h x)
-sector = lookupTree (Proxy :: Proxy (Head (Lookup x xs)))
+sector :: (x ∈ xs) => Lens' (h :* xs) (h x)
+sector = sectorAt membership
 {-# INLINE sector #-}
 
 -- | /O(log n)/ A lens for a value in a known position.
diff --git a/src/Data/Extensible/Sum.hs b/src/Data/Extensible/Sum.hs
--- a/src/Data/Extensible/Sum.hs
+++ b/src/Data/Extensible/Sum.hs
@@ -16,6 +16,8 @@
    (:|)(..)
   , hoist
   , embed
+  , strike
+  , strikeAt
   , (<:|)
   , exhaust
   , picked
@@ -39,6 +41,16 @@
 embed :: (x ∈ xs) => h x -> h :| xs
 embed = UnionAt membership
 {-# INLINE embed #-}
+
+strike :: forall h x xs. (x ∈ xs) => h :| xs -> Maybe (h x)
+strike = strikeAt membership
+{-# INLINE strike #-}
+
+strikeAt :: forall h x xs. Membership xs x -> h :| xs -> Maybe (h x)
+strikeAt q (UnionAt p h) = case compareMembership p q of
+  Right Refl -> Just h
+  _ -> Nothing
+{-# INLINE strikeAt #-}
 
 -- | /O(1)/ Naive pattern match
 (<:|) :: (h x -> r) -> (h :| xs -> r) -> h :| (x ': xs) -> r