diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,3 +1,10 @@
 # Changelog for refinery
 
+
+* 0.1.0.0
+  Initial Release of the library
+
 ## Unreleased changes
+
+* 0.2.0.0
+  Added Alternative/MonadPlus instances to ProofStateT, TacticT, RuleT
diff --git a/refinery.cabal b/refinery.cabal
--- a/refinery.cabal
+++ b/refinery.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.31.1.
+-- This file has been generated from package.yaml by hpack version 0.33.0.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: f61ff60d97eac2723f257e2cb25ede1205a5cb260049a1708c66c7ab0d4669f8
+-- hash: 47bfe1a8a6266a80890a145e94605cb2fc4b85749382b27f0f5ed1db65241473
 
 name:           refinery
-version:        0.1.0.0
+version:        0.2.0.0
 synopsis:       Toolkit for building proof automation systems
 description:    Please see the README on GitHub at <https://github.com/githubuser/refinery#readme>
 category:       Language
@@ -36,31 +36,32 @@
       Paths_refinery
   hs-source-dirs:
       src
+  ghc-options: -Wall -Wredundant-constraints
   build-depends:
       base >=4.7 && <5
-    , containers >=0.5
     , exceptions >=0.10
+    , logict >=0.6
     , mmorph >=1
     , mtl >=2
-    , pipes >=4
-    , semigroupoids >=5
   default-language: Haskell2010
 
 test-suite refinery-test
   type: exitcode-stdio-1.0
   main-is: Spec.hs
   other-modules:
+      Checkers
       Paths_refinery
   hs-source-dirs:
       test
-  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  ghc-options: -Wall -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
   build-depends:
-      base >=4.7 && <5
-    , containers >=0.5
+      QuickCheck
+    , base >=4.7 && <5
+    , checkers
     , exceptions >=0.10
+    , hspec
+    , logict >=0.6
     , mmorph >=1
     , mtl >=2
-    , pipes >=4
     , refinery
-    , semigroupoids >=5
   default-language: Haskell2010
diff --git a/src/Refinery/ProofState.hs b/src/Refinery/ProofState.hs
--- a/src/Refinery/ProofState.hs
+++ b/src/Refinery/ProofState.hs
@@ -1,7 +1,18 @@
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-name-shadowing #-}
+
+{-# LANGUAGE TupleSections          #-}
+{-# LANGUAGE DefaultSignatures      #-}
+{-# LANGUAGE DeriveGeneric          #-}
+{-# LANGUAGE DerivingStrategies     #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE LambdaCase             #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Refinery.ProofState
@@ -11,62 +22,213 @@
 --
 --
 module Refinery.ProofState
-  ( ProofStateT(..)
-  , axiom
-  , mapExtract
-  )
 where
 
-import Control.Applicative
-import Control.Monad
-import Control.Monad.Trans
-import Control.Monad.Catch
-import Control.Monad.Except
-import Control.Monad.Reader.Class
-import Control.Monad.State.Class
-import Control.Monad.IO.Class
+import           Control.Applicative
+import           Control.Monad
+import           Control.Monad.Catch hiding (handle)
+import           Control.Monad.Except
+import qualified Control.Monad.Writer.Lazy as LW
+import qualified Control.Monad.Writer.Strict as SW
+import           Control.Monad.State
+import           Control.Monad.Logic
+import           Control.Monad.Morph
+import           Control.Monad.Reader
 
-import Pipes.Core
+import           GHC.Generics
 
-newtype ProofStateT ext m jdg = ProofStateT { unProofStateT :: Client jdg ext m ext }
+data ProofStateT ext' ext err s m goal
+    = Subgoal goal (ext' -> ProofStateT ext' ext err s m goal)
+    | Effect (m (ProofStateT ext' ext err s m goal))
+    | Stateful (s -> (s, ProofStateT ext' ext err s m goal))
+    | Alt (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)
+    | Interleave (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)
+    | Empty
+    | Failure err
+    | Axiom ext
+    deriving stock (Generic)
 
-instance (Monad m) => Functor (ProofStateT ext m) where
-  fmap f (ProofStateT p) = ProofStateT $ (request . f) >\\ p
+instance (Show goal, Show err, Show ext, Show (m (ProofStateT ext' ext err s m goal))) => Show (ProofStateT ext' ext err s m goal) where
+  show (Subgoal goal _) = "(Subgoal " <> show goal <> " <k>)"
+  show (Effect m) = "(Effect " <> show m <> ")"
+  show (Stateful _) = "(Stateful <s>)"
+  show (Alt p1 p2) = "(Alt " <> show p1 <> " " <> show p2 <> ")"
+  show (Interleave p1 p2) = "(Interleave " <> show p1 <> " " <> show p2 <> ")"
+  show Empty = "Empty"
+  show (Failure err) = "(Failure " <> show err <> ")"
+  show (Axiom ext) = "(Axiom " <> show ext <> ")"
 
-instance (Monad m) => Applicative (ProofStateT ext m) where
-  pure a = ProofStateT $ request a
-  (ProofStateT pf) <*> (ProofStateT pa) = ProofStateT $ (\f -> (request . f) >\\ pa) >\\ pf
+instance Functor m => Functor (ProofStateT ext' ext err s m) where
+    fmap f (Subgoal goal k) = Subgoal (f goal) (fmap f . k)
+    fmap f (Effect m) = Effect (fmap (fmap f) m)
+    fmap f (Stateful s) = Stateful $ fmap (fmap f) . s
+    fmap f (Alt p1 p2) = Alt (fmap f p1) (fmap f p2)
+    fmap f (Interleave p1 p2) = Interleave (fmap f p1) (fmap f p2)
+    fmap _ Empty = Empty
+    fmap _ (Failure err) = Failure err
+    fmap _ (Axiom ext) = Axiom ext
 
-instance (Monad m) => Monad (ProofStateT ext m) where
-  return = pure
-  (ProofStateT p) >>= k = ProofStateT $ (unProofStateT . k) >\\ p
+instance Functor m => Applicative (ProofStateT ext ext err s m) where
+    pure = return
+    (<*>) = ap
 
-instance MonadTrans (ProofStateT ext) where
-  lift m = ProofStateT $ request =<< (lift m)
+instance MFunctor (ProofStateT ext' ext err s) where
+  hoist nat (Subgoal a k) = Subgoal a $ fmap (hoist nat) k
+  hoist nat (Effect m)    = Effect $ nat $ fmap (hoist nat) m
+  hoist nat (Stateful f)    = Stateful $ fmap (hoist nat) . f
+  hoist nat (Alt p1 p2)   = Alt (hoist nat p1) (hoist nat p2)
+  hoist nat (Interleave p1 p2)   = Interleave (hoist nat p1) (hoist nat p2)
+  hoist _ (Failure err) = Failure err
+  hoist _ Empty         = Empty
+  hoist _ (Axiom ext)   = Axiom ext
 
-instance (MonadIO m) => MonadIO (ProofStateT ext m) where
-  liftIO m = ProofStateT $ request =<< (liftIO m)
+applyCont
+    :: (Functor m)
+    => (ext -> ProofStateT ext ext err s m a)
+    -> ProofStateT ext ext err s m a
+    -> ProofStateT ext ext err s m a
+applyCont k (Subgoal goal k') = Subgoal goal (applyCont k . k')
+applyCont k (Effect m) = Effect (fmap (applyCont k) m)
+applyCont k (Stateful s) = Stateful $ fmap (applyCont k) . s
+applyCont k (Alt p1 p2) = Alt (applyCont k p1) (applyCont k p2)
+applyCont k (Interleave p1 p2) = Interleave (applyCont k p1) (applyCont k p2)
+applyCont _ Empty = Empty
+applyCont _ (Failure err) = (Failure err)
+applyCont k (Axiom ext) = k ext
 
-instance (MonadError err m) => MonadError err (ProofStateT ext m) where
-  throwError e = ProofStateT $ lift $ throwError e
-  catchError (ProofStateT m) h = ProofStateT $ catchError m (unProofStateT . h)
+instance Functor m => Monad (ProofStateT ext ext err s m) where
+    return goal = Subgoal goal Axiom
+    (Subgoal a k) >>= f = applyCont ((>>= f) . k) (f a)
+    (Effect m)    >>= f = Effect (fmap (>>= f) m)
+    (Stateful s)  >>= f = Stateful $ fmap (>>= f) . s
+    (Alt p1 p2)   >>= f = Alt (p1 >>= f) (p2 >>= f)
+    (Interleave p1 p2)   >>= f = Interleave (p1 >>= f) (p2 >>= f)
+    (Failure err) >>= _ = Failure err
+    Empty         >>= _ = Empty
+    (Axiom ext)   >>= _ = Axiom ext
 
-instance (MonadThrow m) => MonadThrow (ProofStateT ext m) where
-  throwM e = ProofStateT $ lift $ throwM e
+instance MonadTrans (ProofStateT ext ext err s) where
+    lift m = Effect (fmap pure m)
 
-instance (MonadCatch m) => MonadCatch (ProofStateT ext m) where
-  catch (ProofStateT m) h = ProofStateT $ catch m (unProofStateT . h)
+instance (Monad m) => Alternative (ProofStateT ext ext err s m) where
+    empty = Empty
+    (<|>) = Alt
 
-instance (MonadReader env m) => MonadReader env (ProofStateT ext m) where
-  ask = lift ask
-  local f (ProofStateT m) = ProofStateT $ local f m
+instance (Monad m) => MonadPlus (ProofStateT ext ext err s m) where
+    mzero = empty
+    mplus = (<|>)
 
-instance (MonadState s m) => MonadState s (ProofStateT ext m) where
-  get = lift get
-  put = lift . put
+class (Monad m) => MonadExtract ext m | m -> ext where
+  -- | Generates a "hole" of type @ext@, which should represent
+  -- an incomplete extract.
+  hole :: m ext
+  default hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext
+  hole = lift hole
 
-axiom :: (Monad m) => ext -> ProofStateT ext m jdg
-axiom e = ProofStateT $ return e
+instance (MonadExtract ext m) => MonadExtract ext (ReaderT r m)
+instance (MonadExtract ext m) => MonadExtract ext (StateT s m)
+instance (MonadExtract ext m, Monoid w) => MonadExtract ext (LW.WriterT w m)
+instance (MonadExtract ext m, Monoid w) => MonadExtract ext (SW.WriterT w m)
+instance (MonadExtract ext m) => MonadExtract ext (ExceptT err m)
 
-mapExtract :: (Monad m) => (ext -> ext') -> (ext' -> ext) -> ProofStateT ext m jdg -> ProofStateT ext' m jdg
-mapExtract into out p = ProofStateT $ fmap into ((\j ->  fmap out $ request j) >\\ (unProofStateT p))
+proofs :: forall ext err s m goal. (MonadExtract ext m) => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, [goal])]
+proofs s p = go s [] p
+    where
+      go s goals (Subgoal goal k) = do
+         h <- hole
+         (go s (goals ++ [goal]) $ k h)
+      go s goals (Effect m) = go s goals =<< m
+      go s goals (Stateful f) =
+          let (s', p) = f s
+          in go s' goals p
+      go s goals (Alt p1 p2) = liftA2 (<>) (go s goals p1) (go s goals p2)
+      go s goals (Interleave p1 p2) = liftA2 (interleave) (go s goals p1) (go s goals p2)
+      go _ _ Empty = pure []
+      go _ _ (Failure err) = pure [throwError err]
+      go _ goals (Axiom ext) = pure [Right (ext, goals)]
+
+accumEither :: (Semigroup a, Semigroup b) => Either a b -> Either a b -> Either a b
+accumEither (Left a1) (Left a2)   = Left (a1 <> a2)
+accumEither (Right b1) (Right b2) = Right (b1 <> b2)
+accumEither Left{} x              = x
+accumEither x Left{}              = x
+
+instance (MonadIO m) => MonadIO (ProofStateT ext ext err s m) where
+  liftIO = lift . liftIO
+
+instance (MonadThrow m) => MonadThrow (ProofStateT ext ext err s m) where
+  throwM = lift . throwM
+
+instance (MonadCatch m) => MonadCatch (ProofStateT ext ext err s m) where
+    catch (Subgoal goal k) handle = Subgoal goal (flip catch handle . k)
+    catch (Effect m) handle = Effect . catch m $ pure . handle
+    catch (Stateful s) handle = Stateful (fmap (flip catch handle) . s)
+    catch (Alt p1 p2) handle = Alt (catch p1 handle) (catch p2 handle)
+    catch (Interleave p1 p2) handle = Interleave (catch p1 handle) (catch p2 handle)
+    catch Empty _ = Empty
+    catch (Failure err) _ = Failure err
+    catch (Axiom e) _ = (Axiom e)
+
+instance (Monad m) => MonadError err (ProofStateT ext ext err s m) where
+    throwError = Failure
+    catchError (Subgoal goal k) handle = Subgoal goal (flip catchError handle . k)
+    catchError (Effect m) handle = Effect (fmap (flip catchError handle) m)
+    catchError (Stateful s) handle = Stateful $ fmap (flip catchError handle) . s
+    catchError (Alt p1 p2) handle = catchError p1 handle <|> catchError p2 handle
+    catchError (Interleave p1 p2) handle = catchError p1 handle <|> catchError p2 handle
+    catchError Empty _ = Empty
+    catchError (Failure err) handle = handle err
+    catchError (Axiom e) _ = (Axiom e)
+
+instance (MonadReader r m) => MonadReader r (ProofStateT ext ext err s m) where
+    ask = lift ask
+    local f (Subgoal goal k) = Subgoal goal (local f . k)
+    local f (Effect m) = Effect (local f m)
+    local f (Stateful s) = Stateful (fmap (local f) . s)
+    local f (Alt p1 p2) = Alt (local f p1) (local f p2)
+    local f (Interleave p1 p2) = Interleave (local f p1) (local f p2)
+    local _ Empty = Empty
+    local _ (Failure err) = (Failure err)
+    local _ (Axiom e) = (Axiom e)
+
+instance (Monad m) => MonadState s (ProofStateT ext ext err s m) where
+    state f = Stateful $ \s ->
+      let (a, s') = f s
+      in (s', pure a)
+
+axiom :: ext -> ProofStateT ext' ext err s m jdg
+axiom = Axiom
+
+subgoals :: (Functor m) => [jdg -> ProofStateT ext ext err s m jdg] -> ProofStateT ext ext err s m jdg  -> ProofStateT ext ext err s m jdg
+subgoals [] (Subgoal goal k) = applyCont k (pure goal)
+subgoals (f:fs) (Subgoal goal k)  = applyCont (subgoals fs . k) (f goal)
+subgoals fs (Effect m) = Effect (fmap (subgoals fs) m)
+subgoals fs (Stateful s) = Stateful (fmap (subgoals fs) . s)
+subgoals fs (Alt p1 p2) = Alt (subgoals fs p1) (subgoals fs p2)
+subgoals fs (Interleave p1 p2) = Interleave (subgoals fs p1) (subgoals fs p2)
+subgoals _ (Failure err) = Failure err
+subgoals _ Empty = Empty
+subgoals _ (Axiom ext) = Axiom ext
+
+mapExtract :: (Functor m) => (ext -> ext') -> (ext' -> ext) -> ProofStateT ext ext err s m jdg -> ProofStateT ext' ext' err s m jdg
+mapExtract into out = \case
+    Subgoal goal k -> Subgoal goal $ mapExtract into out . k . out
+    Effect m -> Effect (fmap (mapExtract into out) m)
+    Stateful s -> Stateful (fmap (mapExtract into out) . s)
+    Alt t1 t2 -> Alt (mapExtract into out t1) (mapExtract into out t2)
+    Interleave t1 t2 -> Interleave (mapExtract into out t1) (mapExtract into out t2)
+    Empty -> Empty
+    Failure err -> Failure err
+    Axiom ext -> Axiom $ into ext
+
+mapExtract' :: Functor m => (a -> b) -> ProofStateT ext' a err s m jdg -> ProofStateT ext' b err s m jdg
+mapExtract' into = \case
+    Subgoal goal k -> Subgoal goal $ mapExtract' into . k
+    Effect m -> Effect (fmap (mapExtract' into) m)
+    Stateful s -> Stateful (fmap (mapExtract' into) . s)
+    Alt t1 t2 -> Alt (mapExtract' into t1) (mapExtract' into t2)
+    Interleave t1 t2 -> Interleave (mapExtract' into t1) (mapExtract' into t2)
+    Empty -> Empty
+    Failure err -> Failure err
+    Axiom ext -> Axiom $ into ext
+
diff --git a/src/Refinery/Tactic.hs b/src/Refinery/Tactic.hs
--- a/src/Refinery/Tactic.hs
+++ b/src/Refinery/Tactic.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
@@ -18,129 +19,79 @@
   , runTacticT
   -- * Tactic Combinators
   , (<@>)
+  , (<%>)
   , try
   , many_
   , choice
   , progress
+  , MonadLogic(..)
   -- * Subgoal Manipulation
   , goal
   , focus
-  , forSubgoals
   -- * Tactic Creation
   , MonadExtract(..)
   , MonadRule(..)
   , RuleT
   , rule
-  , MonadProvable(..)
-  , ProvableT(..)
-  , Provable
-  , runProvable
-  -- * Re-Exports
-  , Alt(..)
   ) where
 
-import Data.Functor.Alt
 import Control.Applicative
 import Control.Monad.Except
-import Control.Monad.Reader
 import Control.Monad.State.Strict
-import Control.Monad.Trans
-import Control.Monad.IO.Class
-import Control.Monad.Morph
-
-import Data.Bifunctor
-
-import Pipes.Core
-import Pipes.Lift (runStateP)
+import Control.Monad.Logic
 
 import Refinery.ProofState
 import Refinery.Tactic.Internal
 
--- | Create a tactic that applies each of the tactics in the list to one subgoal.
---
--- When the number of subgoals is greater than the number of provided tactics,
--- the identity tactic is applied to the remainder. When the number of subgoals is
--- less than the number of provided tactics, the remaining tactics are ignored.
-(<@>) :: (MonadProvable jdg m) => TacticT jdg ext m () -> [TacticT jdg ext m ()] -> TacticT jdg ext m ()
-t <@> ts = stateful t applyTac (ts ++ repeat (pure ()))
-  where
-    applyTac j = do
-      tac <- gets head
-      modify tail
-      hoist lift $ asRule j tac
+-- -- | Create a tactic that applies each of the tactics in the list to one subgoal.
+-- --
+-- -- When the number of subgoals is greater than the number of provided tactics,
+-- -- the identity tactic is applied to the remainder. When the number of subgoals is
+-- -- less than the number of provided tactics, the remaining tactics are ignored.
+(<@>) :: (Functor m) => TacticT jdg ext err s m a -> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
+t <@> ts = tactic $ \j -> subgoals (fmap (\t' (_,j') -> proofState t' j') ts) (proofState t j)
 
+infixr 3 <%>
+
+(<%>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
+t1 <%> t2 = tactic $ \j -> Interleave (proofState t1 j) (proofState t2 j)
+
+
 -- | Tries to run a tactic, backtracking on failure
-try :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()
-try t = t <!> pure ()
+try :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
+try t = t <|> pure ()
 
 -- | Runs a tactic repeatedly until it fails
-many_ :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()
+many_ :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
 many_ t = try (t >> many_ t)
 
 -- | Get the current goal
-goal :: (Monad m) => TacticT jdg ext m jdg
+goal :: (Functor m) => TacticT jdg ext err s m jdg
 goal = TacticT $ get
 
-
--- | @choice err ts@ tries to apply a series of tactics @ts@, and commits to the
--- 1st tactic that succeeds. If they all fail, then @err@ is thrown
-choice :: (MonadProvable jdg m, MonadError err m) => err -> [TacticT jdg ext m a] -> TacticT jdg ext m a
-choice err [] = throwError err
-choice err (t:ts) = t <!> choice err ts
+choice :: (Monad m) => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
+choice [] = empty
+choice (t:ts) = t <%> choice ts
 
--- | @progress eq err t@ applies the tactic @t@, and checks to see if the
--- resulting subgoals are all equal to the initial goal by using @eq@. If they
--- are, it throws @err@.
-progress :: (MonadProvable jdg m, MonadError err m) => (jdg -> jdg -> Bool) -> err ->  TacticT jdg ext m a -> TacticT jdg ext m a
+-- -- | @progress eq err t@ applies the tactic @t@, and checks to see if the
+-- -- resulting subgoals are all equal to the initial goal by using @eq@. If they
+-- -- are, it throws @err@.
+progress :: (Monad m) => (jdg -> jdg -> Bool) -> err ->  TacticT jdg ext err s m a -> TacticT jdg ext err s m a
 progress eq err t = do
   j <- goal
   a <- t
   j' <- goal
   if j `eq` j' then pure a else throwError err
 
--- | Apply the first tactic, and then apply the second tactic focused on the @n@th subgoal.
-focus :: (MonadProvable jdg m, Monad m) => TacticT jdg ext m () -> Int -> TacticT jdg ext m () -> TacticT jdg ext m ()
-focus t ix t' = stateful t applyTac 0
-  where
-    applyTac j = do
-      n <- get
-      put (n + 1)
-      hoist lift $ asRule j (if n == ix then t' else pure ())
-
--- | Applies @f@ to every subgoals resulting from the tactic @t@.
-forSubgoals :: (Monad m) => TacticT jdg ext m a -> (jdg -> m b) -> TacticT jdg ext m a
-forSubgoals t f = TacticT $ StateT $ \j -> ProofStateT $
-   action >\\ (unProofStateT $ runStateT (unTacticT t) j)
-  where
-    action (a, j) = do
-      lift $ f j
-      request (a, j)
-
--- | Runs a tactic, producing the extract, along with a list of unsolved subgoals.
-runTacticT :: (MonadExtract ext m) => TacticT jdg ext m () -> jdg -> m (ext, [jdg])
-runTacticT (TacticT t) j =
-  fmap (second reverse) $ flip runStateT [] $ runEffect $ server +>> (hoist lift $ unProofStateT $ execStateT t j)
-  where
-    server :: (MonadExtract ext m) => jdg -> Server jdg ext (StateT [jdg] m) ext
-    server j = do
-      modify (j:)
-      h <- hole
-      respond h >>= server
-
-class (Monad m) => MonadExtract ext m | m -> ext where
-  -- | Generates a "hole" of type @ext@, which should represent
-  -- an incomplete extract.
-  hole :: m ext
-  default hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext
-  hole = lift hole
-
-instance (MonadExtract ext m) => MonadExtract ext (Proxy a' a b' b m)
-instance (MonadExtract ext m) => MonadExtract ext (StateT s m)
-instance (MonadExtract ext m) => MonadExtract ext (ReaderT env m)
-instance (MonadExtract ext m) => MonadExtract ext (ExceptT err m)
-instance (MonadExtract ext m) => MonadExtract ext (RuleT jdg ext m)
+-- -- | Apply the first tactic, and then apply the second tactic focused on the @n@th subgoal.
+focus :: (Functor m) => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
+focus t n t' = t <@> (replicate n (pure ()) ++ [t'] ++ repeat (pure ()))
 
+-- | Runs a tactic, producing a list of possible extracts, along with a list of unsolved subgoals.
+runTacticT :: (MonadExtract ext m) => TacticT jdg ext err s m () -> jdg -> s -> m [Either err (ext, [jdg])]
+runTacticT t j s = proofs s $ fmap snd $ proofState t j
 
 -- | Turn an inference rule into a tactic.
-rule :: (Monad m) => (jdg -> RuleT jdg ext m ext) -> TacticT jdg ext m ()
-rule r = TacticT $ StateT $ \j -> ProofStateT $ (\j' -> request ((), j')) >\\ unRuleT (r j)
+rule :: (Monad m) => (jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
+rule r = tactic $ \j -> fmap ((),) $ unRuleT (r j)
+
diff --git a/src/Refinery/Tactic/Internal.hs b/src/Refinery/Tactic/Internal.hs
--- a/src/Refinery/Tactic/Internal.hs
+++ b/src/Refinery/Tactic/Internal.hs
@@ -1,14 +1,17 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE DefaultSignatures          #-}
+{-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE DerivingStrategies         #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE FunctionalDependencies     #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE DefaultSignatures #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE TupleSections              #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE UndecidableInstances       #-}
+
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Refinery.Tactic.Internal
@@ -22,34 +25,26 @@
 -- change at any given time.
 module Refinery.Tactic.Internal
   ( TacticT(..)
+  , tactic
+  , proofState
   , mapTacticT
-  , stateful
-  , asRule
   , MonadRule(..)
   , RuleT(..)
-  , mapRuleT
-  , MonadProvable(..)
-  , ProvableT(..)
-  , Provable
-  , runProvable
   )
 where
 
-import Data.Functor.Alt
+import GHC.Generics
 import Control.Applicative
 import Control.Monad.Identity
 import Control.Monad.Except
 import Control.Monad.Catch
 import Control.Monad.Reader
 import Control.Monad.State.Strict
-import Control.Monad.Trans
-import Control.Monad.IO.Class
+import Control.Monad.Trans ()
+import Control.Monad.IO.Class ()
 import Control.Monad.Morph
 
-import Data.Bifunctor
-
-import Pipes.Core
-import Pipes.Lift (evalStateP, runStateP)
+import Data.Coerce
 
 import Refinery.ProofState
 
@@ -58,107 +53,120 @@
 --
 -- * @jdg@ - The goal type. This is the thing we are trying to construct a proof of.
 -- * @ext@ - The extract type. This is what we will recieve after running the tactic.
--- * @m@ - The base monad.
--- * @a@ - The return value. This to make @'TacticT'@ a monad, and will always be @'()'@
-newtype TacticT jdg ext m a = TacticT { unTacticT :: StateT jdg (ProofStateT ext m) a }
+-- * @err@ - The error type. We can use 'throwError' to abort the computation with a provided error
+-- * @s@   - The state type.
+-- * @m@   - The base monad.
+-- * @a@   - The return value. This to make @'TacticT'@ a monad, and will always be @'()'@
+newtype TacticT jdg ext err s m a = TacticT { unTacticT :: StateT jdg (ProofStateT ext ext err s m) a }
   deriving ( Functor
+           , Applicative
+           , Alternative
+           , Monad
+           , MonadPlus
            , MonadReader env
            , MonadError err
            , MonadIO
            , MonadThrow
            , MonadCatch
+           , Generic
            )
 
-instance (MonadProvable jdg m) => Applicative (TacticT jdg ext m) where
-  pure a = TacticT $ StateT $ proving >=> \j -> pure (a, j)
-  (<*>) = ap
+instance (Monoid jdg, Show a, Show jdg, Show err, Show ext, Show (m (ProofStateT ext ext err s m (a, jdg)))) => Show (TacticT jdg ext err s m a) where
+  show = show . flip runStateT mempty . unTacticT
 
-instance (MonadProvable jdg m) => Monad (TacticT jdg ext m) where
-  return = pure
-  t >>= k = TacticT $ StateT $ proving >=> \j -> do
-    (a, j') <- runStateT (unTacticT t) j
-    runStateT (unTacticT $ k a) =<< proving j'
+-- | Helper function for producing a tactic.
+tactic :: (jdg -> ProofStateT ext ext err s m (a, jdg)) -> TacticT jdg ext err s m a
+tactic t = TacticT $ StateT t
 
+-- |  Helper function for deconstructing a tactic.
+proofState :: TacticT jdg ext err s m a -> jdg -> ProofStateT ext ext err s m (a, jdg)
+proofState t j = runStateT (unTacticT t) j
+
 -- | Map the unwrapped computation using the given function
-mapTacticT :: (Monad m) => (m a -> m b) -> TacticT jdg ext m a -> TacticT jdg ext m b
+mapTacticT :: (Monad m) => (m a -> m b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
 mapTacticT f (TacticT m) = TacticT $ m >>= (lift . lift . f . return)
 
-instance (MonadError err m) => Alt (TacticT jdg ext m) where
-  (TacticT t1) <!> (TacticT t2) = TacticT $ t1 `catchError` (const t2)
-
-instance MonadTrans (TacticT jdg ext) where
+instance MonadTrans (TacticT jdg ext err s) where
   lift m = TacticT $ lift $ lift m
 
-instance (MonadProvable jdg m, MonadState s m) => MonadState s (TacticT jdg ext m) where
-  get = lift get
-  put = lift . put
+instance (Monad m) => MonadState s (TacticT jdg ext err s m) where
+    state f = tactic $ \j -> fmap (,j) $ state f
 
--- | Helper function for making "stateful" tactics like "<@>"
-stateful :: (Monad m) => TacticT jdg ext m a -> (jdg -> RuleT jdg ext (StateT s m) ext) -> s -> TacticT jdg ext m a
-stateful (TacticT t) f s = TacticT $ StateT $ \j -> ProofStateT $
-  evalStateP s $ action >\\ (hoist lift $ unProofStateT $ runStateT t j)
-  where
-    action (a, j) = (\j' -> request (a, j')) >\\ (unRuleT $ f j)
+-- | A @'RuleT'@ is a monad transformer for creating inference rules.
+newtype RuleT jdg ext err s m a = RuleT
+  { unRuleT :: ProofStateT ext a err s m jdg
+  }
+  deriving stock Generic
 
--- | Transforms a tactic into a rule. Useful for doing things with @'stateful'@.
-asRule :: (Monad m) => jdg -> TacticT jdg ext m a -> RuleT jdg ext m ext
-asRule j t = RuleT $ unProofStateT $ execStateT (unTacticT t) j
+instance (Show jdg, Show err, Show a, Show (m (ProofStateT ext a err s m jdg))) => Show (RuleT jdg ext err s m a) where
+  show = show . unRuleT
 
--- | A @'RuleT'@ is a monad transformer for creating inference rules.
-newtype RuleT jdg ext m a = RuleT { unRuleT :: Client jdg ext m a }
-  deriving ( Functor
-           , Applicative
-           , Monad
-           , MonadReader env
-           , MonadState s
-           , MonadError err
-           , MonadIO
-           , MonadThrow
-           , MonadCatch
-           , MonadTrans
-           , MFunctor
-           )
+instance Functor m => Functor (RuleT jdg ext err s m) where
+  fmap = coerce mapExtract'
 
+instance Monad m => Applicative (RuleT jdg ext err s m) where
+  pure = return
+  (<*>) = ap
 
--- | Map the unwrapped computation using the given function
-mapRuleT :: (Monad m) => (m a -> m b) -> RuleT jdg ext m a -> RuleT jdg ext m b
-mapRuleT f (RuleT m) = RuleT $ m >>= (lift . f . return)
+instance Monad m => Monad (RuleT jdg ext err s m) where
+  return = coerce . Axiom
+  RuleT (Subgoal goal k)   >>= f = coerce $ Subgoal goal $ fmap (bindAlaCoerce f) k
+  RuleT (Effect m)         >>= f = coerce $ Effect $ fmap (bindAlaCoerce f) m
+  RuleT (Stateful s)       >>= f = coerce $ Stateful $ fmap (bindAlaCoerce f) . s
+  RuleT (Alt p1 p2)        >>= f = coerce $ Alt (bindAlaCoerce f p1) (bindAlaCoerce f p2)
+  RuleT (Interleave p1 p2) >>= f = coerce $ Interleave (bindAlaCoerce f p1) (bindAlaCoerce f p2)
+  RuleT Empty              >>= _ = coerce $ Empty
+  RuleT (Failure err)      >>= _ = coerce $ Failure err
+  RuleT (Axiom e)          >>= f = f e
 
+instance Monad m => MonadState s (RuleT jdg ext err s m) where
+    state f = RuleT $ Stateful $ \s ->
+        let (a, s') = f s
+        in (s', Axiom a)
+
+instance MonadReader r m => MonadReader r (RuleT jdg ext err s m) where
+    ask = lift ask
+    local f (RuleT (Subgoal goal k))   = coerce $ Subgoal goal (localAlaCoerce f . k)
+    local f (RuleT (Effect m))         = coerce $ Effect (local f m)
+    local f (RuleT (Stateful s))       = coerce $ Stateful (fmap (localAlaCoerce f) . s)
+    local f (RuleT (Alt p1 p2))        = coerce $ Alt (localAlaCoerce f p1) (localAlaCoerce f p2)
+    local f (RuleT (Interleave p1 p2)) = coerce $ Interleave (localAlaCoerce f p1) (localAlaCoerce f p2)
+    local _ (RuleT Empty)              = coerce $ Empty
+    local _ (RuleT (Failure err))      = coerce $ Failure err
+    local _ (RuleT (Axiom e))          = coerce $ Axiom e
+
+bindAlaCoerce
+  :: (Monad m, Coercible c (m b), Coercible a1 (m a2)) =>
+     (a2 -> m b) -> a1 -> c
+bindAlaCoerce f = coerce . (f =<<) . coerce
+
+localAlaCoerce
+  :: (MonadReader r m) =>
+     (r -> r) -> ProofStateT ext a err s m jdg -> ProofStateT ext a err s m jdg
+localAlaCoerce f = coerce . local f . RuleT
+
+instance MonadTrans (RuleT jdg ext err s) where
+  lift = coerce . Effect . fmap Axiom
+
+instance MFunctor (RuleT jdg ext err s) where
+  hoist nat = hoist nat . coerce
+
+instance MonadIO m => MonadIO (RuleT jdg ext err s m) where
+  liftIO = lift . liftIO
+
+instance Monad m => MonadError err (RuleT jdg ext err s m) where
+  throwError = coerce . Failure
+  catchError r h = coerce $ flip catchError h $ coerce r
+
 class (Monad m) => MonadRule jdg ext m | m -> jdg, m -> ext where
   -- | Create a subgoal, and return the resulting extract.
   subgoal :: jdg -> m ext
   default subgoal :: (MonadTrans t, MonadRule jdg ext m1, m ~ t m1) => jdg -> m ext
   subgoal = lift . subgoal
 
-instance (Monad m) => MonadRule jdg ext (RuleT jdg ext m) where
-  subgoal j = RuleT $ request j
+instance (Monad m) => MonadRule jdg ext (RuleT jdg ext err s m) where
+  subgoal j = RuleT $ Subgoal j Axiom
 
 instance (MonadRule jdg ext m) => MonadRule jdg ext (ReaderT env m)
 instance (MonadRule jdg ext m) => MonadRule jdg ext (StateT env m)
 instance (MonadRule jdg ext m) => MonadRule jdg ext (ExceptT env m)
-instance (MonadRule jdg ext m) => MonadRule jdg ext (ProvableT env m)
-
-class (Monad m) => MonadProvable jdg m | m -> jdg where
-  -- | Applies a transformation of goals at every step of the tactic.
-  proving :: jdg -> m jdg
-  default proving :: (MonadTrans t, MonadProvable jdg m1, m ~ t m1) => jdg -> m jdg
-  proving = lift . proving
-
-instance (MonadProvable jdg m) => MonadProvable jdg (ProofStateT ext m)
-instance (MonadProvable jdg m) => MonadProvable jdg (ReaderT r m)
-instance (MonadProvable jdg m) => MonadProvable jdg (StateT s m)
-instance (MonadProvable jdg m) => MonadProvable jdg (ExceptT err m)
-instance (Monad m) => MonadProvable jdg (ProvableT jdg m) where
-  proving = pure
-
--- | Helper newtype for when you don't have any need for the mechanisms of MonadProvable.
-newtype ProvableT jdg m a = ProvableT { runProvableT :: m a }
-  deriving (Functor, Applicative, Monad, MonadIO, MonadState s, MonadError err)
-
-type Provable jdg a = ProvableT jdg Identity a
-
-instance MonadTrans (ProvableT jdg) where
-  lift = ProvableT
-
-runProvable :: Provable jdg a -> a
-runProvable = runIdentity . runProvableT
diff --git a/test/Checkers.hs b/test/Checkers.hs
new file mode 100644
--- /dev/null
+++ b/test/Checkers.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+
+module Checkers where
+
+import Control.Monad.State.Class
+import Test.QuickCheck hiding (Failure)
+import Test.QuickCheck.Checkers
+
+monadState
+    :: forall m s a b
+     . ( MonadState s m
+       , EqProp (m s)
+       , EqProp (m ())
+       , Show s
+       , Arbitrary s
+       )
+    => m (a, b)
+    -> TestBatch
+monadState _ =
+  ( "MonadState laws"
+  , [ ("get >> get", (get >> get) =-= get @s @m)
+    , ("get >>= put", (get @s @m >>= put) =-= pure ())
+    , ("put >> put", property $ do
+        s1 <- arbitrary
+        s2 <- arbitrary
+        pure $
+          counterexample (show s1) $
+          counterexample (show s2) $
+            (put @_ @m s1 >> put s2) =-= put s2
+      )
+    , ("put >> get", property $ do
+        s <- arbitrary
+        pure $
+          counterexample (show s) $
+            (put s >> get) =-= pure @m s
+      )
+    ]
+  )
+
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -1,2 +1,209 @@
+{-# LANGUAGE DeriveAnyClass             #-}
+{-# LANGUAGE DerivingStrategies         #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE StandaloneDeriving         #-}
+{-# LANGUAGE TypeApplications           #-}
+{-# LANGUAGE UndecidableInstances       #-}
+{-# OPTIONS_GHC -Wredundant-constraints #-}
+{-# OPTIONS_GHC -fno-warn-orphans       #-}
+
+module Main where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.State.Strict (StateT (..))
+import Control.Monad.State.Class
+import Data.Function
+import Data.Functor.Identity
+import Data.Monoid (Sum (..))
+import Refinery.ProofState
+import Refinery.Tactic
+import Refinery.Tactic.Internal
+import Test.Hspec
+import Test.QuickCheck hiding (Failure)
+import Test.QuickCheck.Checkers
+import Test.QuickCheck.Classes
+import Checkers
+
+testBatch :: TestBatch -> Spec
+testBatch (batchName, tests) = describe ("laws for: " ++ batchName) $
+  foldr (>>) (return ()) (map (uncurry it) tests)
+
+
+instance (MonadExtract ext m, EqProp (m [Either err (ext, [a])]), Arbitrary s)
+      => EqProp (ProofStateT ext ext err s m a) where
+  (=-=) a b = property $ do
+    s <- arbitrary
+    pure $ ((=-=) `on` proofs s) a b
+
+instance ( Show jdg
+         , MonadExtract ext m
+         , Arbitrary jdg
+         , EqProp (m [Either err (ext, [jdg])])
+         , Show s
+         , Arbitrary s
+         )
+      => EqProp (TacticT jdg ext err s m a) where
+  (=-=) = (=-=) `on` runTacticT . (() <$)
+
+instance ( Show jdg
+         , Arbitrary jdg
+         , EqProp (m [Either err (ext, [jdg])])
+         , MonadExtract ext m
+         , Show s
+         , Arbitrary s
+         )
+      => EqProp (RuleT jdg ext err s m ext) where
+  (=-=) = (=-=) `on` rule . const
+
+instance MonadExtract Int Identity where
+  hole = pure 0
+
+instance ( CoArbitrary ext'
+         , Arbitrary ext
+         , Arbitrary err
+         , Arbitrary a
+         , Arbitrary (m (ProofStateT ext' ext err s m a))
+         , CoArbitrary s
+         , Arbitrary s
+         )
+      => Arbitrary (ProofStateT ext' ext err s m a) where
+  arbitrary = getSize >>= \case
+    n | n <= 1 -> oneof small
+    _ -> oneof $
+      [ Subgoal <$> decayArbitrary 2 <*> decayArbitrary 2
+      , Effect  <$> arbitrary
+      , Alt     <$> decayArbitrary 2 <*> decayArbitrary 2
+      , Stateful <$> arbitrary
+      ] ++ small
+    where
+      small =
+        [ pure Empty
+        , Failure <$> arbitrary
+        , Axiom   <$> arbitrary
+        ]
+  shrink = genericShrink
+
+instance (Arbitrary (m (a, s)), CoArbitrary s) => Arbitrary (StateT s m a) where
+  arbitrary = StateT <$> arbitrary
+
+instance ( CoArbitrary jdg
+         , Arbitrary a
+         , Arbitrary ext
+         , Arbitrary err
+         , CoArbitrary ext
+         , Arbitrary jdg
+         , Arbitrary (m (ProofStateT ext ext err s m (a, jdg)))
+         , CoArbitrary s
+         , Arbitrary s
+         )
+      => Arbitrary (TacticT jdg ext err s m a) where
+  arbitrary = fmap (TacticT . StateT) arbitrary
+  shrink = genericShrink
+
+instance ( Arbitrary a
+         , Arbitrary err
+         , CoArbitrary ext
+         , Arbitrary jdg
+         , Arbitrary (m (ProofStateT ext a err s m jdg))
+         , CoArbitrary s
+         , Arbitrary s
+         )
+      => Arbitrary (RuleT jdg ext err s m a) where
+  arbitrary = fmap RuleT arbitrary
+  shrink = genericShrink
+
+decayArbitrary :: Arbitrary a => Int -> Gen a
+decayArbitrary n = scale (`div` n) arbitrary
+
+type ProofStateTest = ProofStateT Int Int String Int Identity
+type RuleTest = RuleT Int Int String Int Identity
+type TacticTest = TacticT (Sum Int) Int String Int Identity
+
 main :: IO ()
-main = putStrLn "Test suite not yet implemented"
+main = hspec $ do
+  describe "ProofStateT" $ do
+    testBatch $ functor     (undefined :: ProofStateTest (Int, Int, Int))
+    testBatch $ applicative (undefined :: ProofStateTest (Int, Int, Int))
+    testBatch $ alternative (undefined :: ProofStateTest Int)
+    testBatch $ monad       (undefined :: ProofStateTest (Int, Int, Int))
+    testBatch $ monadPlus   (undefined :: ProofStateTest (Int, Int))
+    testBatch $ monadState  (undefined :: ProofStateTest (Int, Int))
+    it "distrib put over <|>" $ property $ distribPut (undefined :: ProofStateTest (Int))
+  describe "RuleT" $ do
+    testBatch $ functor     (undefined :: RuleTest (Int, Int, Int))
+    testBatch $ applicative (undefined :: RuleTest (Int, Int, Int))
+    testBatch $ monad       (undefined :: RuleTest (Int, Int, Int))
+  describe "TacticT" $ do
+    testBatch $ functor     (undefined :: TacticTest ((), (), ()))
+    testBatch $ applicative (undefined :: TacticTest ((), (), ()))
+    testBatch $ alternative (undefined :: TacticTest ())
+    testBatch $ monad       (undefined :: TacticTest ((), (), ()))
+    testBatch $ monadPlus   (undefined :: TacticTest ((), ()))
+    testBatch $ monadState  (undefined :: TacticTest ((), ()))
+    it "interleave - mzero" $ property $ interleaveMZero (undefined :: TacticTest Int)
+    it "interleave - mplus" $ property $ interleaveMPlus (undefined :: TacticTest Int)
+    it "distrib put over <|>" $ property $ distribPut (undefined :: TacticTest ())
+
+leftAltBind
+    :: forall m a b
+    . (EqProp (m b), Monad m, Alternative m)
+    => m a -> m a -> (a -> m b)
+    -> Property
+leftAltBind m1 m2 f =
+  ((m1 <|> m2) >>= f) =-= ((m1 >>= f) <|> (m2 >>= f))
+
+rightAltBind
+    :: forall m a
+    . (EqProp (m a), Monad m, Alternative m)
+    => m () -> m a -> m a
+    -> Property
+rightAltBind m1 m2 m3 =
+  (m1 >> (m2 <|> m3)) =-= ((m1 >> m2) <|> (m1 >> m3))
+
+interleaveMZero
+    :: forall m a jdg ext err s
+     . (MonadExtract ext m, EqProp (m [Either err (ext, [jdg])]),
+      Show jdg, Show s, Arbitrary jdg, Arbitrary s)
+    => TacticT jdg ext err s m a  -- ^ proxy
+    -> TacticT jdg ext err s m a
+    -> Property
+interleaveMZero _ m =
+    (mzero <%> m) =-= m
+
+interleaveMPlus
+    :: forall m a jdg ext err s
+     . (MonadExtract ext m, EqProp (m [Either err (ext, [jdg])]),
+      Show jdg, Show s, Arbitrary jdg, Arbitrary s)
+    => TacticT jdg ext err s m a  -- ^ proxy
+    -> a
+    -> TacticT jdg ext err s m a
+    -> TacticT jdg ext err s m a
+    -> Property
+interleaveMPlus _ a m1 m2 =
+    ((pure a <|> m1) <%> m2) =-= (pure a <|> (m2 <%> m1))
+
+distribPut
+    :: forall s m a
+     . ( MonadState s m
+       , Alternative m
+       , EqProp (m a)
+       , Arbitrary (m a)
+       , Arbitrary s
+       , Show s
+       , Show (m a)
+       )
+    => m a -> Property
+distribPut _ = property $ do
+  s <- arbitrary @s
+  m1 <- arbitrary @(m a)
+  m2 <- arbitrary @(m a)
+  pure $
+    counterexample (show s) $
+    counterexample (show m1) $
+    counterexample (show m2) $
+      (put s >> (m1 <|> m2)) =-= ((put s >> m1) <|> (put s >> m2))
+