diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,11 @@
 # Changelog for the `parameterized-utils` package
 
+## 2.1.1 -- *2020 Jul 30*
+
+  * Added `drop` and `appendEmbeddingLeft` functions to the `Context` module.
+  * Fixes/updates to haddock documentation (fixing Issue #74).
+  * Allow tasty v1.3 for testing (thanks to felixonmars)
+
 ## 2.1.0 -- *2020 May 08*
 
   * Added `plusAssoc` to the `NatRepr` module to produce `+` associativity evidence.
diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,5 +1,5 @@
 Name:          parameterized-utils
-Version:       2.1.0
+Version:       2.1.1
 Author:        Galois Inc.
 Maintainer:    jhendrix@galois.com, kquick@galois.com
 stability:     stable
@@ -19,7 +19,7 @@
 extra-source-files: Changelog.md
 homepage:      https://github.com/GaloisInc/parameterized-utils
 bug-reports:   https://github.com/GaloisInc/parameterized-utils/issues
-tested-with:   GHC==8.4.4, GHC==8.6.5, GHC==8.8.3, GHC==8.10.1
+tested-with:   GHC==8.6.5, GHC==8.8.3, GHC==8.10.1
 
 -- Many (but not all, sadly) uses of unsafe operations are
 -- controlled by this compile flag.  When this flag is set
@@ -38,7 +38,7 @@
   build-depends: base >= 4.10 && < 5
                , base-orphans   >=0.8.2 && <0.9
                , th-abstraction >=0.3  && <0.4
-               , constraints    >=0.10 && <0.12
+               , constraints    >=0.10 && <0.13
                , containers
                , deepseq
                , ghc-prim
@@ -116,7 +116,7 @@
                , lens
                , mtl
                , parameterized-utils
-               , tasty == 1.2.*
+               , tasty >= 1.2 && < 1.4
                , tasty-ant-xml == 1.1.*
                , tasty-hunit >= 0.9 && < 0.11
                , tasty-hedgehog
diff --git a/src/Data/Parameterized/Context.hs b/src/Data/Parameterized/Context.hs
--- a/src/Data/Parameterized/Context.hs
+++ b/src/Data/Parameterized/Context.hs
@@ -56,6 +56,7 @@
   , Data.Parameterized.Context.last
   , Data.Parameterized.Context.view
   , Data.Parameterized.Context.take
+  , Data.Parameterized.Context.drop
   , forIndexM
   , generateSome
   , generateSomeM
@@ -75,6 +76,7 @@
   , extendEmbeddingRight
   , extendEmbeddingBoth
   , appendEmbedding
+  , appendEmbeddingLeft
   , ctxeSize
   , ctxeAssignment
 
@@ -238,11 +240,16 @@
 view :: forall f ctx . Assignment f ctx -> AssignView f ctx
 view = viewAssign
 
+-- | Return the prefix of an appended 'Assignment'
 take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
 take sz sz' asgn =
   let diff = appendDiff sz' in
   generate sz (\i -> asgn ! extendIndex' diff i)
 
+-- | Return the suffix of an appended 'Assignment'
+drop :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'
+drop sz sz' asgn = generate sz' (\i -> asgn ! extendIndexAppendLeft sz sz' i)
+
 --------------------------------------------------------------------------------
 -- Context embedding.
 
@@ -310,10 +317,15 @@
 extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
 extendEmbeddingRight = extendEmbeddingRightDiff knownDiff
 
+-- | Prove that the prefix of an appended context is embeddable in it
 appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
 appendEmbedding sz sz' = CtxEmbedding (addSize sz sz') (generate sz (extendIndex' diff))
   where
   diff = appendDiff sz'
+
+-- | Prove that the suffix of an appended context is embeddable in it
+appendEmbeddingLeft :: Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')
+appendEmbeddingLeft sz sz' = CtxEmbedding (addSize sz sz') (generate sz' (extendIndexAppendLeft sz sz'))
 
 extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
 extendEmbeddingBoth ctxe = updated & ctxeAssignment %~ flip extend (nextIndex (ctxe ^. ctxeSize))
diff --git a/src/Data/Parameterized/Context/Safe.hs b/src/Data/Parameterized/Context/Safe.hs
--- a/src/Data/Parameterized/Context/Safe.hs
+++ b/src/Data/Parameterized/Context/Safe.hs
@@ -77,6 +77,7 @@
   , nextIndex
   , extendIndex
   , extendIndex'
+  , extendIndexAppendLeft
   , forIndex
   , forIndexRange
   , intIndex
@@ -308,9 +309,19 @@
 extendIndex = extendIndex' knownDiff
 
 {-# INLINE extendIndex' #-}
+-- | Compute an 'Index' into a context @r@ from an 'Index' into
+-- a sub-context @l@ of @r@.
 extendIndex' :: Diff l r -> Index l tp -> Index r tp
 extendIndex' DiffHere idx = idx
 extendIndex' (DiffThere diff) idx = IndexThere (extendIndex' diff idx)
+
+{-# INLINE extendIndexAppendLeft #-}
+-- | Compute an 'Index' into an appended context from an 'Index' into
+-- its suffix.
+extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
+extendIndexAppendLeft sz sz' idx = case viewIndex sz' idx of
+  IndexViewLast _ -> lastIndex (addSize sz sz')
+  IndexViewInit idx' -> skipIndex (extendIndexAppendLeft sz (decSize sz') idx')
 
 -- | Given a size @n@, an initial value @v0@, and a function @f@, the
 -- expression @forIndex n v0 f@ calls @f@ on each index less than @n@
diff --git a/src/Data/Parameterized/Context/Unsafe.hs b/src/Data/Parameterized/Context/Unsafe.hs
--- a/src/Data/Parameterized/Context/Unsafe.hs
+++ b/src/Data/Parameterized/Context/Unsafe.hs
@@ -49,6 +49,7 @@
   , nextIndex
   , extendIndex
   , extendIndex'
+  , extendIndexAppendLeft
   , forIndex
   , forIndexRange
   , intIndex
@@ -268,8 +269,16 @@
 extendIndex = extendIndex' knownDiff
 
 {-# INLINE extendIndex' #-}
+-- | Compute an 'Index' into a context @r@ from an 'Index' into
+-- a sub-context @l@ of @r@.
 extendIndex' :: Diff l r -> Index l tp -> Index r tp
 extendIndex' _ = unsafeCoerce
+
+{-# INLINE extendIndexAppendLeft #-}
+-- | Compute an 'Index' into an appended context from an 'Index' into
+-- its suffix.
+extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
+extendIndexAppendLeft (Size l) _ (Index idx) = Index (idx + l)
 
 -- | Given a size @n@, an initial value @v0@, and a function @f@, the
 -- expression @forIndex n v0 f@ is equivalent to @v0@ when @n@ is
diff --git a/src/Data/Parameterized/NatRepr.hs b/src/Data/Parameterized/NatRepr.hs
--- a/src/Data/Parameterized/NatRepr.hs
+++ b/src/Data/Parameterized/NatRepr.hs
@@ -387,7 +387,7 @@
     GT -> NatCaseGT (unsafeCoerce (LeqProof :: LeqProof 0 0))
 {-# NOINLINE testNatCases #-}
 
--- | The strict order (<), defined by n < m <-> n + 1 <= m, is irreflexive.
+-- | The strict order (\<), defined by n \< m \<-> n + 1 \<= m, is irreflexive.
 lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void
 lessThanIrreflexive a prf =
   let prf1 :: LeqProof (1 + a - a) (a - a)
@@ -400,7 +400,7 @@
       prf4 = case prf2 of Refl -> case prf3 of { Refl -> prf1 }
   in case prf4 of {}
 
--- | The strict order on the naturals is irreflexive.
+-- | The strict order on the naturals is asymmetric
 lessThanAsymmetric :: forall m f n
                     . LeqProof (n+1) m
                    -> LeqProof (m+1) n
diff --git a/test/Test/Context.hs b/test/Test/Context.hs
--- a/test/Test/Context.hs
+++ b/test/Test/Context.hs
@@ -11,6 +11,7 @@
 import           Control.Lens
 import           Data.Parameterized.Classes
 import qualified Data.Parameterized.Context as C
+import qualified Data.Parameterized.Ctx.Proofs as P
 import qualified Data.Parameterized.Context.Safe as S
 import qualified Data.Parameterized.Context.Unsafe as U
 import           Data.Parameterized.Some
@@ -172,6 +173,48 @@
           Just Refl -> vals1 === vals2
           Nothing   -> vals1 /== vals2
 
+   , testProperty "take none" $ property $
+     do vals1 <- forAll genSomePayloadList
+        vals2 <- forAll genSomePayloadList
+        vals3 <- forAll genSomePayloadList
+        Some w <- return $ mkUAsgn vals1
+        Some x <- return $ mkUAsgn vals2
+        Some y <- return $ mkUAsgn vals3
+        let z = w U.<++> x U.<++> y
+        case P.leftId z of
+          Refl -> let r = C.take U.zeroSize (U.size z) z in
+                    assert $ isJust $ testEquality U.empty r
+   , testProperty "drop none" $ property $
+     do vals1 <- forAll genSomePayloadList
+        vals2 <- forAll genSomePayloadList
+        vals3 <- forAll genSomePayloadList
+        Some w <- return $ mkUAsgn vals1
+        Some x <- return $ mkUAsgn vals2
+        Some y <- return $ mkUAsgn vals3
+        let z = w U.<++> x U.<++> y
+        case P.leftId z of
+          Refl -> let r = C.drop U.zeroSize (U.size z) z in
+                    assert $ isJust $ testEquality z r
+   , testProperty "take all" $ property $
+     do vals1 <- forAll genSomePayloadList
+        vals2 <- forAll genSomePayloadList
+        vals3 <- forAll genSomePayloadList
+        Some w <- return $ mkUAsgn vals1
+        Some x <- return $ mkUAsgn vals2
+        Some y <- return $ mkUAsgn vals3
+        let z = w U.<++> x U.<++> y
+        let r = C.take (U.size z) U.zeroSize z
+        assert $ isJust $ testEquality z r
+   , testProperty "drop all" $ property $
+     do vals1 <- forAll genSomePayloadList
+        vals2 <- forAll genSomePayloadList
+        vals3 <- forAll genSomePayloadList
+        Some w <- return $ mkUAsgn vals1
+        Some x <- return $ mkUAsgn vals2
+        Some y <- return $ mkUAsgn vals3
+        let z = w U.<++> x U.<++> y
+        let r = C.drop (U.size z) U.zeroSize z
+        assert $ isJust $ testEquality U.empty r
    , testProperty "append_take" $ property $
      do vals1 <- forAll genSomePayloadList
         vals2 <- forAll genSomePayloadList
@@ -180,5 +223,37 @@
         let z = x U.<++> y
         let x' = C.take (U.size x) (U.size y) z
         assert $ isJust $ testEquality x x'
-
+   , testProperty "append_take_drop" $ property $
+     do vals1 <- forAll genSomePayloadList
+        vals2 <- forAll genSomePayloadList
+        Some x <- return $ mkUAsgn vals1
+        Some y <- return $ mkUAsgn vals2
+        let z = x U.<++> y
+        let x' = C.take (U.size x) (U.size y) z
+        let y' = C.drop (U.size x) (U.size y) z
+        assert $ isJust $ testEquality x x'
+        assert $ isJust $ testEquality y y'
+   , testProperty "append_take_drop_multiple" $ property $
+     do vals1 <- forAll genSomePayloadList
+        vals2 <- forAll genSomePayloadList
+        vals3 <- forAll genSomePayloadList
+        vals4 <- forAll genSomePayloadList
+        vals5 <- forAll genSomePayloadList
+        Some u <- return $ mkUAsgn vals1
+        Some v <- return $ mkUAsgn vals2
+        Some w <- return $ mkUAsgn vals3
+        Some x <- return $ mkUAsgn vals4
+        Some y <- return $ mkUAsgn vals5
+        let uv = u U.<++> v
+        let wxy = w U.<++> x U.<++> y
+        -- let z = u C.<++> v C.<++> w C.<++> x C.<++> y
+        let z = uv U.<++> wxy
+        let uv' = C.take (U.size uv) (U.size wxy) z
+        let wxy' = C.drop (U.size uv) (U.size wxy) z
+        let withWXY = C.dropPrefix z uv (error "failed dropPrefix")
+        assert $ isJust $ testEquality (u U.<++> v) uv'
+        assert $ isJust $ testEquality (w U.<++> x U.<++> y) wxy'
+        assert $ isJust $ testEquality uv uv'
+        assert $ isJust $ testEquality wxy wxy'
+        withWXY $ \t -> assert $ isJust $ testEquality wxy' t
    ]