diff --git a/compdata.cabal b/compdata.cabal
--- a/compdata.cabal
+++ b/compdata.cabal
@@ -1,5 +1,5 @@
 Name:			compdata
-Version:		0.8.1.1
+Version:		0.8.1.2
 Synopsis:            	Compositional Data Types
 Description:
 
diff --git a/src/Data/Comp/SubsumeCommon.hs b/src/Data/Comp/SubsumeCommon.hs
--- a/src/Data/Comp/SubsumeCommon.hs
+++ b/src/Data/Comp/SubsumeCommon.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances #-}
+{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances, TypeOperators #-}
 
 --------------------------------------------------------------------------------
 -- |
@@ -14,35 +14,119 @@
 --
 --------------------------------------------------------------------------------
 
-module Data.Comp.SubsumeCommon where
+module Data.Comp.SubsumeCommon
+    ( ComprEmb
+    , Pos (..)
+    , Emb (..)
+    ) where
 
+-- | This type is used in its promoted form only. It represents
+-- pointers from the left-hand side of a subsumption to the right-hand
+-- side.
 data Pos = Here | Le Pos | Ri Pos | Sum Pos Pos
+
+-- | This type is used in its promoted form only. It represents
+-- possible results for checking for subsumptions. 'Found' indicates a
+-- subsumption was found; 'NotFound' indicates no such subsumption was
+-- found. 'Ambiguous' indicates that there are duplicates on the left-
+-- or the right-hand side.
 data Emb = Found Pos | NotFound | Ambiguous
 
+-- | This type family takes a position type and compresses it. That
+-- means it replaces each nested occurrence of 
+-- 
+-- @
+--   Sum (prefix (Le Here)) (prefix (Ri Here))@
+-- @
+---
+-- with 
+-- 
+-- @
+--   prefix Here@
+-- @
+-- 
+-- where @prefix@ is some composition of @Le@ and @Ri@. The rational
+-- behind this type family is that it provides a more compact proof
+-- term of a subsumption, and thus yields more efficient
+-- implementations of 'inj' and 'prj'.
+
 type family ComprPos (p :: Pos) :: Pos where
     ComprPos Here = Here
     ComprPos (Le p) = Le (ComprPos p)
     ComprPos (Ri p) = Ri (ComprPos p)
     ComprPos (Sum l r) = CombineMaybe (Sum l r) (Combine (ComprPos l) (ComprPos r))
 
+-- | Helper type family for 'ComprPos'.
 type family CombineMaybe (p :: Pos) (p' :: Maybe Pos) where
     CombineMaybe p (Just p') = p'
     CombineMaybe p p'        = p
 
+
+-- | Helper type family for 'ComprPos'.
 type family Combine (l :: Pos) (r :: Pos) :: Maybe Pos where
     Combine (Le l) (Le r) = Le' (Combine l r)
     Combine (Ri l) (Ri r) = Ri' (Combine l r)
     Combine (Le Here) (Ri Here) = Just Here
     Combine l r = Nothing
 
+-- | 'Ri' lifted to 'Maybe'.
 type family Ri' (p :: Maybe Pos) :: Maybe Pos where
     Ri' Nothing = Nothing
     Ri' (Just p) = Just (Ri p)
 
+-- | 'Le' lifted to 'Maybe'.
 type family Le' (p :: Maybe Pos) :: Maybe Pos where
     Le' Nothing = Nothing
     Le' (Just p) = Just (Le p)
 
+
+-- | If the argument is not 'Found', this type family is the
+-- identity. Otherwise, the argument is of the form @Found p@, and
+-- this type family does two things: (1) it checks whether @p@ the
+-- contains duplicates; and (2) it compresses @p@ using 'ComprPos'. If
+-- (1) finds no duplicates, @Found (ComprPos p)@ is returned;
+-- otherwise @Ambiguous@ is returned.
+-- 
+-- For (1) it is assumed that @p@ does not contain 'Sum' nested
+-- underneath a 'Le' or 'Ri' (i.e. only at the root or underneath a
+-- 'Sum'). We will refer to such positions below as /atomic position/.
+-- Positions not containing 'Sum' are called /simple positions/.
 type family ComprEmb (e :: Emb) :: Emb where
-    ComprEmb (Found p) = Found (ComprPos p)
+    ComprEmb (Found p) = Check (Dupl p) (ComprPos p)
     ComprEmb e = e
+
+-- | Helper type family for 'ComprEmb'.
+type family Check (b :: Bool) (p :: Pos) where
+    Check False p = Found p
+    Check True  p = Ambiguous
+
+-- | This type family turns a list of /atomic position/ into a list of
+-- /simple positions/ by recursively splitting each position of the
+-- form @Sum p1 p2@ into @p1@ and @p2@.
+type family ToList (s :: [Pos]) :: [Pos] where
+    ToList (Sum p1 p2 ': s) = ToList (p1 ': p2 ': s)
+    ToList (p ': s) = p ': ToList s
+    ToList '[] = '[]
+
+-- | This type checks whether the argument (atomic) position has
+-- duplicates.
+type Dupl s = Dupl' (ToList '[s])
+
+-- | This type family checks whether the list of positions given as an
+-- argument contains any duplicates.
+type family Dupl' (s :: [Pos]) :: Bool where
+    Dupl' (p ': r) = OrDupl' (Find p r) r
+    Dupl' '[] = False
+
+-- | This type family checks whether its first argument is contained
+-- its second argument.
+type family Find (p :: Pos) (s :: [Pos]) :: Bool where
+    Find p (p ': r)  = True
+    Find p (p' ': r) = Find p r
+    Find p '[] = False
+
+-- | This type family returns @True@ if the first argument is true;
+-- otherwise it checks the second argument for duplicates.
+type family OrDupl' (a :: Bool) (b :: [Pos]) :: Bool where
+    OrDupl'  True  c  = True
+    OrDupl'  False c  = Dupl' c