diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,12 @@
 # Changelog for polysemy-check
 
+## v0.3.0.0 (2021-10-09)
+
+- `prepropLaw` now synthesizes a monadic prelude and postlude to your laws, to
+    ensure they hold under every context. The type has changed as a result.
+- `prepropEquivalent` now allows you to produce a functor `f` result, so you can
+    check equivalence of the underlying state as well.
+
 ## v0.2.0.0 (2021-10-09)
 
 - Updated the signature of `prepropEquivalent` to take a `Proxy r`. This lets
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.2.0.0
+version:        0.3.0.0
 synopsis:       QuickCheck for Polysemy
 description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy-check#readme>
 category:       Polysemy
diff --git a/src/Polysemy/Check.hs b/src/Polysemy/Check.hs
--- a/src/Polysemy/Check.hs
+++ b/src/Polysemy/Check.hs
@@ -29,6 +29,7 @@
   , GenericK
   ) where
 
+import Control.Monad (void)
 import Data.Proxy
 import Generics.Kind (GenericK)
 import Generics.Kind.TH (deriveGenericK)
@@ -102,18 +103,37 @@
 -- For example, any lawful interpretation of @State@ must satisfy the @put s1
 -- >> put s2 = put s2@ law.
 prepropLaw
-    :: (Eq x, Show x)
+    :: forall effs r a f
+     . ( (forall z. Eq z => Eq (f z))
+       , (forall z. Show z => Show (f z))
+       )
+    => ( Eq a
+       , Show a
+       , ArbitraryEff effs r
+       )
     => Gen (Sem r a, Sem r a)
        -- ^ A generator for two equivalent programs.
-    -> (Sem r a -> IO x)
+    -> (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 $ do
+prepropLaw g lower = property @(Gen Property) $ do
+  SomeEff pre <- arbitraryActionFromRow @effs @r
   (m1, m2) <- g
+  SomeEff post <- arbitraryActionFromRow @effs @r
   pure $ ioProperty $ do
-    a1 <- lower m1
-    a2 <- lower m2
+    a1 <-
+      lower $ do
+        void $ send pre
+        a1 <- m1
+        r <- send post
+        pure (a1, r)
+    a2 <-
+      lower $ do
+        void $ send pre
+        a2 <- m2
+        r <- send post
+        pure (a2, r)
     pure $ a1 === a2
 
 
@@ -122,12 +142,15 @@
 -- property ensures that the two interpreters give the same result for every
 -- arbitrary program.
 prepropEquivalent
-    :: forall effs x r1 r2
-     . (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs)
-    => (forall a. Sem r1 a -> IO a)
+    :: forall effs x r1 r2 f
+     . ( forall a. Show a => Show (f a)
+       , forall a. Eq a => Eq (f a)
+       )
+    => (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs)
+    => (forall a. Sem r1 a -> IO (f a))
        -- ^ The first interpreter for the effect stack.Pure effect stacks can
        -- be lifted into 'IO' via 'pure' after the final 'run'.
-    -> (forall a. Sem r2 a -> IO a)
+    -> (forall a. Sem r2 a -> IO (f a))
        -- ^ The second interpreter to prove equivalence for.
     -> (forall r. Proxy r -> Members effs r => Gen (Sem r x))
        -- ^ A generator producing arbitrary programs in @r@. The property will
diff --git a/test/EquivSpec.hs b/test/EquivSpec.hs
--- a/test/EquivSpec.hs
+++ b/test/EquivSpec.hs
@@ -5,7 +5,7 @@
 
 module EquivSpec where
 
-import Data.IORef (newIORef)
+import Data.IORef (newIORef, readIORef)
 import Data.Proxy (Proxy)
 import Polysemy
 import Polysemy.Check
@@ -30,12 +30,14 @@
             pure $ send e1 >> send e2 >> send e3
 
 
-runPureState :: Int -> Sem '[State Int] a -> IO a
-runPureState s = pure . run . evalState s
+runPureState :: Int -> Sem '[State Int] a -> IO (Int, a)
+runPureState s = pure . run . runState s
 
 
-runIOState :: Int -> Sem '[State Int, Embed IO] a -> IO (a)
+runIOState :: Int -> Sem '[State Int, Embed IO] a -> IO (Int, a)
 runIOState s sem = do
   ref <- newIORef s
-  runM . runStateIORef ref $ sem
+  a <- runM . runStateIORef ref $ sem
+  r <- readIORef ref
+  pure (r, a)
 
diff --git a/test/LawSpec.hs b/test/LawSpec.hs
--- a/test/LawSpec.hs
+++ b/test/LawSpec.hs
@@ -37,28 +37,38 @@
 
 
 putPutLaw
-    :: (Arbitrary s, Member (State s) r, Eq x, Show x)
-    => (Sem r s -> IO x)
+    :: forall s r
+     . ( Arbitrary s
+       , Member (State s) r
+       , Eq s
+       , Show s
+       , ArbitraryEff '[State s] r
+       )
+    => (forall a. Sem r ((), a) -> IO (s, ((), a)))
     -> Property
-putPutLaw = prepropLaw $ do
+putPutLaw = prepropLaw @'[State s] $ do
   s1 <- arbitrary
   s2 <- arbitrary
   pure
     ( do
         put s1
         put s2
-        get
     , do
         put s2
-        get
     )
 
 
 getPutLaw
-    :: (Arbitrary s, Member (State s) r, Eq x, Show x)
-    => (Sem r () -> IO x)
+    :: forall s r
+     . ( Arbitrary s
+       , Member (State s) r
+       , Eq s
+       , Show s
+       , ArbitraryEff '[State s] r
+       )
+    => (forall a. Sem r ((), a) -> IO (s, ((), a)))
     -> Property
-getPutLaw = prepropLaw $ do
+getPutLaw = prepropLaw @'[State s] $ do
   pure
     ( get >>= put
     , pure ()
@@ -66,10 +76,16 @@
 
 
 putGetLaw
-    :: (Arbitrary s, Member (State s) r, Eq x, Show x)
-    => (Sem r s -> IO x)
+    :: forall s r
+     . ( Arbitrary s
+       , Member (State s) r
+       , Eq s
+       , Show s
+       , ArbitraryEff '[State s] r
+       )
+    => (forall a. Sem r (s, a) -> IO (s, (s, a)))
     -> Property
-putGetLaw = prepropLaw $ do
+putGetLaw = prepropLaw @'[State s] $ do
   s <- arbitrary
   pure
     ( do