diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,11 @@
 # Changelog for polysemy-check
 
+## v0.9.0.0 (2021-12-03)
+
+- `prepropLaw` now generates a new `Law` record, allowing for better control
+    over the program prelude and postludes
+- `prepropLaw` now takes a labeler, for running QuickCheck coverage
+
 ## v0.8.1.0 (2021-10-21)
 
 - Added a new function, `prepropAllCommutative` which ensures every effect
diff --git a/polysemy-check.cabal b/polysemy-check.cabal
--- a/polysemy-check.cabal
+++ b/polysemy-check.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           polysemy-check
-version:        0.8.1.0
+version:        0.9.0.0
 synopsis:       QuickCheck for Polysemy
 description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy-check#readme>
 category:       Polysemy
@@ -68,6 +68,7 @@
   type: exitcode-stdio-1.0
   main-is: Main.hs
   other-modules:
+      BigKeySpec
       CommutativeSpec
       CoverageSpec
       EquivSpec
diff --git a/src/Polysemy/Check.hs b/src/Polysemy/Check.hs
--- a/src/Polysemy/Check.hs
+++ b/src/Polysemy/Check.hs
@@ -7,6 +7,10 @@
   , prepropEquivalent
   , prepropLaw
 
+    -- * Law Constructors
+  , Law (..)
+  , simpleLaw
+
     -- * Generators for Effects
   , arbitraryAction
   , arbitraryActionOfType
@@ -18,6 +22,9 @@
   , SomeEff (..)
   , SomeEffOfType (..)
 
+  -- * Common labeling functions
+  , constructorLabel
+
     -- * Support for Existential Types
   , ExistentialFor
 
@@ -43,6 +50,7 @@
 import Polysemy.Internal
 import Polysemy.Internal.Union.Inject (Inject, inject)
 import Test.QuickCheck
+import Data.Data (Data, showConstr, toConstr)
 
 
 ------------------------------------------------------------------------------
@@ -121,6 +129,34 @@
 
 
 ------------------------------------------------------------------------------
+-- | Data structure containing programs that should be equal, and under which
+-- circumstances.
+--
+-- @since 0.9.0.0
+data Law r z a = Law
+  { lawLhs      :: Sem r a
+    -- ^ 'lawLhs' and 'lawRhs' are being asserted as equal.
+  , lawRhs      :: Sem r a
+    -- ^ 'lawLhs' and 'lawRhs' are being asserted as equal.
+  , lawPrelude  :: [Sem r ()]
+    -- ^ A set of actions to possibly run before checking equality. Useful for
+    -- ensuring the existence of something being tested.
+  , lawPostlude :: [Sem r z]
+    -- ^ A set of actions to possibly run after checking equality. Useful for
+    -- checking the existence after something was created.
+  }
+
+
+------------------------------------------------------------------------------
+-- | Like 'Law', but for the common case when you don't need a custom prelude
+-- or postlude.
+--
+-- @since 0.9.0.0
+simpleLaw :: Sem r a -> Sem r a -> Law r () a
+simpleLaw lhs rhs = Law lhs rhs [] []
+
+
+------------------------------------------------------------------------------
 -- | Prove that two programs in @r@ are equivalent under a given
 -- interpretation. This is useful for proving laws about particular effects (or
 -- stacks of effects).
@@ -128,41 +164,80 @@
 -- For example, any lawful interpretation of @State@ must satisfy the @put s1
 -- >> put s2 = put s2@ law.
 prepropLaw
-    :: forall effs r a f
+    :: forall effs x r a f
      . ( (forall z. Eq z => Eq (f z))
        , (forall z. Show z => Show (f z))
        )
     => ( Eq a
        , Show a
+       , Functor f
        , ArbitraryEff effs r
+       , Eq x
+       , Show x
        )
-    => Gen (Sem r a, Sem r a)
+    => Gen (Law r x a)
        -- ^ A generator for two equivalent programs.
+    -> Maybe (f a -> String)
+       -- ^ How to label the results for QuickCheck coverage.
     -> (forall z. Sem r (a, z) -> IO (f (a, z)))
        -- ^ An interpreter for the effect stack down to 'IO'. Pure effect
        -- stacks can be lifted into 'IO' via 'pure' after the final 'run'.
     -> Property
-prepropLaw g lower = property @(Gen Property) $ do
-  SomeEff pre <- arbitraryActionFromRow @effs @r
-  (m1, m2) <- g
-  SomeEff post <- arbitraryActionFromRow @effs @r
+prepropLaw g labeler lower = property @(Gen Property) $ do
+  Law lhs rhs mprel mpost <- g
+  SomeEff pre1 <- arbitraryActionFromRow @effs @r
+  prel <- maybeOneof mprel
+  SomeEff pre2 <- arbitraryActionFromRow @effs @r
+  SomeEff post1 <- arbitraryActionFromRow @effs @r
+  post <- maybeOneof mpost
+  SomeEff post2 <- arbitraryActionFromRow @effs @r
   pure $
-    counterexample ("before = " <> show pre) $
-    counterexample ("after  = " <> show post) $
+    counterexample ("before1 = " <> show pre1) $
+    counterexample ("before2 = " <> show pre2) $
+    counterexample ("after1  = " <> show post1) $
+    counterexample ("after2  = " <> show post2) $
       ioProperty $ do
         a1 <-
           lower $ do
-            void $ send pre
-            a1 <- m1
-            r <- send post
-            pure (a1, r)
+            void $ send pre1
+            void $ prel
+            void $ send pre2
+            a1 <- lhs
+            void $ send post1
+            z <- post
+            r <- send post2
+            pure (a1, (z, r))
         a2 <-
           lower $ do
-            void $ send pre
-            a2 <- m2
-            r <- send post
-            pure (a2, r)
-        pure $ a1 === a2
+            void $ send pre1
+            void prel
+            void $ send pre2
+            a2 <- rhs
+            void $ send post1
+            z <- post
+            r <- send post2
+            pure (a2, (z, r))
+        pure
+          $ maybe property (\lbl -> label $ lbl $ fmap fst a1) labeler
+          $ a1 === a2
+
+
+maybeOneof :: [Sem r a] -> Gen (Sem r (Maybe a))
+maybeOneof [] = pure $ pure Nothing
+maybeOneof res = do
+  chance <- elements @Int [0..9]
+  case chance < 8 of
+    True -> fmap (fmap Just) $ elements res
+    False -> pure $ pure Nothing
+
+
+
+------------------------------------------------------------------------------
+-- | Label an example with its data constructor.
+--
+-- @since 0.9.0.0
+constructorLabel :: Data a => a -> String
+constructorLabel = showConstr . toConstr
 
 
 ------------------------------------------------------------------------------
diff --git a/test/BigKeySpec.hs b/test/BigKeySpec.hs
new file mode 100644
--- /dev/null
+++ b/test/BigKeySpec.hs
@@ -0,0 +1,74 @@
+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
+
+module BigKeySpec where
+
+import qualified Data.Map as M
+import Data.Map (Map)
+import Polysemy
+import Polysemy.Check
+import Test.Hspec
+import Test.QuickCheck
+import Test.Hspec.QuickCheck
+import Polysemy.State
+import Data.Functor.Identity
+import Data.Word
+
+data KVStore k v m a where
+  Store :: k -> v -> KVStore k v m ()
+  Delete :: k -> KVStore k v m ()
+  Retrieve :: k -> KVStore k v m (Maybe v)
+
+deriving instance (Show k, Show v) => Show (KVStore k v m a)
+
+makeSem ''KVStore
+deriveGenericK ''KVStore
+
+
+data Bug = HasBug | NoBug
+
+runKVStore :: forall k v r a. Ord k => Bug -> Sem (KVStore k v ': r) a -> Sem r a
+runKVStore bug = (evalState (mempty @(Map k v)) .) $  reinterpret $ \case
+  Store k v -> modify $ M.insert k v
+  Delete k ->
+    case bug of
+      HasBug -> pure ()
+      NoBug -> modify $ M.delete k
+  Retrieve k -> gets $ M.lookup k
+
+
+deleteGetLaw
+    :: forall r
+     . r ~ '[KVStore Word64 Bool]
+    => Bug
+    -> (Word64 -> Bool -> [Sem r ()])
+    -> Property
+deleteGetLaw bug prel =
+  prepropLaw @r
+    (do
+      k <- arbitrary
+      v <- arbitrary
+      pure $ Law
+        { lawLhs = do
+            delete k
+            retrieve k
+        , lawRhs = do
+            delete k
+            pure Nothing
+        , lawPrelude = prel k v
+        , lawPostlude = [] :: [Sem r ()]
+        }
+    )
+    Nothing  -- (Just $ constructorLabel . runIdentity)
+    (pure . Identity . run . runKVStore @Word64 @Bool bug)
+
+
+spec :: Spec
+spec = do
+  describe "without prelude" $ do
+    -- prop "with bug"    $ deleteGetLaw HasBug $ \_ _ -> []
+    prop "without bug" $ deleteGetLaw NoBug $ \_ _ -> []
+
+  describe "with prelude" $ do
+    prop "with bug"    $ expectFailure $ deleteGetLaw HasBug $ \k v -> [store k v]
+    prop "without bug" $ deleteGetLaw NoBug $ \k v -> [store k v]
+
diff --git a/test/ExampleSpec.hs b/test/ExampleSpec.hs
--- a/test/ExampleSpec.hs
+++ b/test/ExampleSpec.hs
@@ -29,44 +29,40 @@
 spec :: Spec
 spec = do
   describe "Laws" $ do
-    let law x = prepropLaw @'[Stack Int] x $ pure . run . runStack []
+    let law x = prepropLaw @'[Stack Int] x (Just $ constructorLabel . fst) $ pure . run . runStack []
 
     prop "push >> pop is pure" $ do
       law $ do
         s <- arbitrary
-        pure
-          ( push s >> pop
-          , pure $ Just s
-          )
+        pure $ simpleLaw
+          (push s >> pop)
+          (pure $ Just s)
 
     prop "pop >> push is id" $ do
       law $
-        pure
-          ( pop >>= maybe (pure ()) push
-          , pure ()
-          )
+        pure $ simpleLaw
+          (pop >>= maybe (pure ()) push)
+          (pure ())
 
+
     prop "removeAll sets size to 0" $ do
       law $
-        pure
-          ( removeAll >> size
-          , removeAll >> pure 0
-          )
+        pure $ simpleLaw
+          (removeAll >> size)
+          (removeAll >> pure 0)
 
     prop "push increases size by 1" $ do
       law $ do
         s <- arbitrary
-        pure
-          ( push s >> size
-          , fmap (+1) size <* push s
-          )
+        pure $ simpleLaw
+          (push s >> size)
+          (fmap (+1) size <* push s)
 
     prop "pop decreases size by 1" $ do
       law $ do
-        pure
-          ( pop >> size
-          , fmap (max 0 . subtract 1) size <* pop
-          )
+        pure $ simpleLaw
+          (pop >> size)
+          (fmap (max 0 . subtract 1) size <* pop)
 
 
   describe "Equivalence" $ do
diff --git a/test/LawSpec.hs b/test/LawSpec.hs
--- a/test/LawSpec.hs
+++ b/test/LawSpec.hs
@@ -16,24 +16,24 @@
   describe "pure state" $ do
     prop "put >> put = put" $ do
       s <- arbitrary
-      pure $ putPutLaw $ runPureState s
+      pure $ putPutLaw Nothing $ runPureState s
     prop "get >>= put = pure ()" $ do
       s <- arbitrary
-      pure $ getPutLaw $ runPureState s
+      pure $ getPutLaw Nothing $ runPureState s
     prop "put >> get = put >> pure" $ do
       s <- arbitrary
-      pure $ putGetLaw $ runPureState s
+      pure $ putGetLaw Nothing $ runPureState s
 
   describe "io state" $ do
     prop "put >> put = put" $ do
       s <- arbitrary
-      pure $ putPutLaw $ runIOState s
+      pure $ putPutLaw Nothing $ runIOState s
     prop "get >>= put = pure ()" $ do
       s <- arbitrary
-      pure $ getPutLaw $ runIOState s
+      pure $ getPutLaw Nothing $ runIOState s
     prop "put >> get = put >> pure" $ do
       s <- arbitrary
-      pure $ putGetLaw $ runIOState s
+      pure $ putGetLaw Nothing $ runIOState s
 
 
 type LawConstraints f effs s r =
@@ -52,18 +52,18 @@
      . ( res ~ ()
        , LawConstraints f effs s r
        )
-    => (forall a. Sem r (res, a) -> IO (f (res, a)))
+    => Maybe (f res -> String)
+    -> (forall a. Sem r (res, a) -> IO (f (res, a)))
     -> Property
 putPutLaw = prepropLaw @effs $ do
   s1 <- arbitrary
   s2 <- arbitrary
-  pure
+  pure $ simpleLaw
     ( do
         put s1
-        put s2
-    , do
-        put s2
-    )
+        put s2)
+    ( do
+        put s2)
 
 
 getPutLaw
@@ -71,13 +71,13 @@
      . ( res ~ ()
        , LawConstraints f effs s r
        )
-    => (forall a. Sem r (res, a) -> IO (f (res, a)))
+    => Maybe (f res -> String)
+    -> (forall a. Sem r (res, a) -> IO (f (res, a)))
     -> Property
 getPutLaw = prepropLaw @effs $ do
-  pure
-    ( get >>= put
-    , pure ()
-    )
+  pure $ simpleLaw
+    (get >>= put)
+    (pure ())
 
 
 putGetLaw
@@ -85,18 +85,18 @@
      . ( res ~ s
        , LawConstraints f effs s r
        )
-    => (forall a. Sem r (res, a) -> IO (f (res, a)))
+    => Maybe (f res -> String)
+    -> (forall a. Sem r (res, a) -> IO (f (res, a)))
     -> Property
 putGetLaw = prepropLaw @effs $ do
   s <- arbitrary
-  pure
+  pure $ simpleLaw
     ( do
         put s
-        get
-    , do
+        get)
+    ( do
         put s
-        pure s
-    )
+        pure s)
 
 
 runPureState :: Int -> Sem '[State Int] a -> IO (Int, a)