diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs
index 1bc8b7ecb0..7d78045692 100644
--- a/kore/src/Kore/Builtin/Map.hs
+++ b/kore/src/Kore/Builtin/Map.hs
@@ -91,8 +91,6 @@ import           Kore.Step.Simplification.Data
 import           Kore.Step.StepperAttributes
                  ( StepperAttributes )
 import qualified Kore.Step.StepperAttributes as StepperAttributes
-import           Kore.Step.Substitution
-                 ( normalize )
 import           Kore.Unification.Error
                  ( UnificationOrSubstitutionError (..) )
 import           Kore.Unparser
@@ -573,9 +571,9 @@ unifyEquals
 unifyEquals
     simplificationType
     tools
-    substitutionSimplifier
-    simplifier
-    axiomIdToSimplifier
+    _
+    _
+    _
     unifyEqualsChildren
   =
     unifyEquals0
@@ -717,14 +715,7 @@ unifyEquals
                 -- Elements of map2 missing from map1
                 remainder2 = Map.difference map2 map1
 
-        normalized <- Monad.Trans.lift $
-            normalize
-                tools
-                substitutionSimplifier
-                simplifier
-                axiomIdToSimplifier
-                result
-        return (normalized, SimplificationProof)
+        return (result, SimplificationProof)
       where
         Domain.InternalMap { builtinMapSort } = builtin1
         Domain.InternalMap { builtinMapChild = map1 } = builtin1
diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs
index f6a4647268..68f649a141 100644
--- a/kore/src/Kore/Builtin/Set.hs
+++ b/kore/src/Kore/Builtin/Set.hs
@@ -96,8 +96,6 @@ import           Kore.Step.Simplification.Data
 import           Kore.Step.StepperAttributes
                  ( StepperAttributes )
 import qualified Kore.Step.StepperAttributes as StepperAttributes
-import           Kore.Step.Substitution
-                 ( normalize )
 import           Kore.Unification.Error
                  ( UnificationOrSubstitutionError (..) )
 import           Kore.Unparser
@@ -531,9 +529,9 @@ unifyEquals
 unifyEquals
     simplificationType
     tools
-    substitutionSimplifier
-    simplifier
-    axiomIdToSimplifier
+    _
+    _
+    _
     unifyEqualsChildren
   =
     unifyEquals0
@@ -635,14 +633,7 @@ unifyEquals
                     -- Return the concrete set, but capture any predicates and
                     -- substitutions from unifying the framing variable.
                     asExpandedPattern builtinSetSort set1 <* remainder
-            normalized <- Monad.Trans.lift $
-                normalize
-                    tools
-                    substitutionSimplifier
-                    simplifier
-                    axiomIdToSimplifier
-                    result
-            return (normalized, SimplificationProof)
+            return (result, SimplificationProof)
 
       | otherwise =
         return (ExpandedPattern.bottom, SimplificationProof)
diff --git a/kore/src/Kore/Step/Simplification/Data.hs b/kore/src/Kore/Step/Simplification/Data.hs
index df568e2b51..ffddbf84a6 100644
--- a/kore/src/Kore/Step/Simplification/Data.hs
+++ b/kore/src/Kore/Step/Simplification/Data.hs
@@ -11,6 +11,13 @@ module Kore.Step.Simplification.Data
     ( Simplifier
     , runSimplifier
     , evalSimplifier
+    , BranchT, runBranchT
+    , getBranches
+    , liftPruned, returnPruned
+    , evalSimplifierBranch
+    , gather
+    , gatherAll
+    , scatter
     , PredicateSubstitutionSimplifier (..)
     , StepPatternSimplifier (..)
     , SimplificationProof (..)
@@ -18,30 +25,45 @@ module Kore.Step.Simplification.Data
     , Environment (..)
     ) where
 
-import Colog
-       ( HasLog (..), LogAction (..) )
-import Control.Concurrent.MVar
-       ( MVar )
-import Control.Monad.Reader
-import Control.Monad.Trans.Except
-       ( ExceptT (..), runExceptT )
-
-import Kore.AST.Common
-       ( SortedVariable )
-import Kore.AST.MetaOrObject
-import Kore.Logger
-       ( LogMessage )
-import Kore.Step.Pattern
-import Kore.Step.Representation.ExpandedPattern
-       ( PredicateSubstitution )
-import Kore.Step.Representation.OrOfExpandedPattern
-       ( OrOfExpandedPattern )
-import Kore.Unparser
-import Kore.Variables.Fresh
-import SimpleSMT
-       ( Solver )
-import SMT
-       ( MonadSMT, SMT (..), liftSMT, withSolver' )
+import           Colog
+                 ( HasLog (..), LogAction (..) )
+import           Control.Concurrent.MVar
+                 ( MVar )
+import qualified Control.Monad as Monad
+import           Control.Monad.Reader
+import           Control.Monad.State.Class
+                 ( MonadState )
+import qualified Control.Monad.Trans as Monad.Trans
+import           Control.Monad.Trans.Except
+                 ( ExceptT (..), runExceptT )
+import qualified Data.Foldable as Foldable
+import           Data.Typeable
+import           GHC.Stack
+                 ( HasCallStack )
+
+import           Kore.AST.Common
+                 ( SortedVariable )
+import           Kore.AST.MetaOrObject
+import           Kore.Logger
+                 ( LogMessage )
+import           Kore.Step.Pattern
+import           Kore.Step.Representation.ExpandedPattern
+                 ( PredicateSubstitution )
+import           Kore.Step.Representation.MultiOr
+                 ( MultiOr )
+import qualified Kore.Step.Representation.MultiOr as OrOfExpandedPattern
+import           Kore.Step.Representation.OrOfExpandedPattern
+                 ( OrOfExpandedPattern )
+import           Kore.TopBottom
+                 ( TopBottom )
+import qualified Kore.TopBottom as TopBottom
+import           Kore.Unparser
+import           Kore.Variables.Fresh
+import           ListT
+import           SimpleSMT
+                 ( Solver )
+import           SMT
+                 ( MonadSMT, SMT (..), liftSMT, withSolver' )
 
 {-| 'And' simplification is very similar to 'Equals' simplification.
 This type is used to distinguish between the two in the common code.
@@ -54,11 +76,158 @@ simplification of a MetaMLPattern was correct.
 data SimplificationProof level = SimplificationProof
     deriving (Show, Eq)
 
+-- * Branching
+
+{- | 'BranchT' extends any 'Monad' with disjoint branches.
+
+Broadly, one goal of simplification is to promote 'Or' (disjunction) to the top
+level. Many @Simplifier@s return a 'MultiOr' for this reason; we can think of
+this as external branching. @BranchT Simplifier@ also allows branching through
+'Alternative'. Branches are created with '<|>':
+@
+let
+    simplifier1 :: BranchT Simplifier a
+    simplifier2 :: BranchT Simplifier a
+in
+    simplifier1 <|> simplifier2  -- A 'BranchT Simplifier' with two branches.
+@
+
+Branches are pruned with 'empty':
+@
+simplify :: BranchT Simplifier a
+simplify = do
+    unless condition empty
+    continue  -- This simplifier would not be reached if "condition" is 'False'.
+@
+
+Use 'scatter' and 'gather' to translate between the two forms of branches.
+
+-}
+newtype BranchT m a =
+    -- Pay no attention to the ListT behind the curtain!
+    BranchT { runBranchT :: ListT m a }
+    deriving
+        ( Alternative
+        , Applicative
+        , Functor
+        , Monad
+        , MonadIO
+        , MonadPlus
+        , MonadTrans
+        , Typeable
+        )
+
+deriving instance MonadReader r m => MonadReader r (BranchT m)
+
+deriving instance MonadState s m => MonadState s (BranchT m)
+
+instance MonadSMT m => MonadSMT (BranchT m) where
+    liftSMT = lift . liftSMT
+    {-# INLINE liftSMT #-}
+
+{- | Collect the values produced along the disjoint branches.
+ -}
+getBranches :: Applicative m => BranchT m a -> m [a]
+getBranches (BranchT as) = toListM as
+
+{- | Lift a computation into 'BranchT' while pruning 'isBottom' results.
+
+Example:
+
+@
+liftPrune (return 'Kore.Step.ExpandedPattern.bottom') === empty
+@
+
+See also: 'returnPruned'
+
+ -}
+liftPruned :: (Monad m, TopBottom t) => m t -> BranchT m t
+liftPruned unlifted = Monad.Trans.lift unlifted >>= returnPruned
+
+{- | Return a 't' unless the value satisfies 'TopBottom.isBottom'.
+
+When the values satisfies 'TopBottom.isBottom', the result is 'empty' instead.
+
+Example:
+
+@
+returnPruned 'Kore.Step.ExpandedPattern.bottom' === empty
+@
+
+ -}
+returnPruned :: TopBottom t => t -> BranchT m t
+returnPruned t
+  | TopBottom.isBottom t = empty
+  | otherwise = return t
+
+{- | Collect results from many simplification branches into one result.
+
+@gather@ returns all the results of a @'BranchT' m a@ in a single disjunction
+('MultiOr'). @gather@ strips away the @BranchT@ transformer so that it always
+returns one result.
+
+Examples:
+
+@
+gather (pure a <|> pure b) === pure ('OrOfExpandedPattern.make' [a, b])
+@
+
+@
+gather empty === pure ('OrOfExpandedPattern.make' [])
+@
+
+See also: 'scatter'
+
+ -}
+gather :: Applicative m => BranchT m a -> m (MultiOr a)
+gather simpl = OrOfExpandedPattern.MultiOr <$> getBranches simpl
+
+{- | Collect results from many simplification branches into one result.
+
+@gather@ returns all the results of a @'BranchT' m a@ in a single disjunction
+('MultiOr'). @gather@ strips away the @BranchT@ transformer so that it always
+returns one result.
+
+See also: 'scatter', 'gather'
+
+ -}
+gatherAll :: Applicative m => BranchT m (MultiOr a) -> m (MultiOr a)
+gatherAll simpl = Monad.join <$> gather simpl
+
+{- | Disperse results into many simplification branches.
+
+Examples:
+
+@
+scatter ('OrOfExpandedPattern.make' [a, b]) === (pure a <|> pure b)
+@
+
+@
+scatter ('OrOfExpandedPattern.make' []) === empty
+@
+
+See also: 'gather'
+
+ -}
+scatter
+    :: MultiOr a
+    -> BranchT m a
+scatter ors = Foldable.asum (pure <$> ors)
+
+-- * Simplifier
+
 data Environment = Environment
     { solver     :: !(MVar Solver)
     , logger     :: !(LogAction Simplifier LogMessage)
     }
 
+{- | @Simplifier@ represents a simplification action.
+
+A @Simplifier@ can send constraints to the SMT solver through 'MonadSMT'.
+
+A @Simplifier@ can write to the log through 'HasLog'.
+
+ -}
 newtype Simplifier a = Simplifier
     { getSimplifier :: ReaderT Environment IO a
     }
@@ -109,33 +278,51 @@ instance HasLog Environment LogMessage (ExceptT e Simplifier) where
                 res <- runExceptT (action msg)
                 return $ either (const ()) id res
 
-{- | Run a simplifier computation.
+{- | Run a simplification, returning the results along all branches.
+ -}
+evalSimplifierBranch
+    :: LogAction Simplifier LogMessage
+    -- ^ initial counter for fresh variables
+    -> BranchT Simplifier a
+    -- ^ simplifier computation
+    -> SMT [a]
+evalSimplifierBranch logger =
+    evalSimplifier logger . getBranches
+
+{- | Run a simplification, returning the result of only one branch.
 
-  The result is returned along with the final 'Counter'.
+__Warning__: @runSimplifier@ calls 'error' if the 'Simplifier' does not contain
+exactly one branch. Use 'evalSimplifierBranch' to evaluation simplifications
+that may branch.
 
  -}
 runSimplifier
-    :: Simplifier a
+    :: HasCallStack
+    => Simplifier a
     -- ^ simplifier computation
     -> LogAction Simplifier LogMessage
     -- ^ initial counter for fresh variables
     -> SMT a
-runSimplifier (Simplifier s) logger =
-    withSolver' $ \solver -> do
-        a <- runReaderT s $ Environment solver logger
-        pure a
+runSimplifier simpl logger =
+    evalSimplifier logger simpl
 
-{- | Evaluate a simplifier computation.
+{- | Evaluate a simplifier computation, returning the result of only one branch.
 
-Only the result is returned; the counter is discarded.
+__Warning__: @evalSimplifier@ calls 'error' if the 'Simplifier' does not contain
+exactly one branch. Use 'evalSimplifierBranch' to evaluation simplifications
+that may branch.
 
   -}
 evalSimplifier
-    :: LogAction Simplifier LogMessage
+    :: HasCallStack
+    => LogAction Simplifier LogMessage
     -> Simplifier a
     -> SMT a
-evalSimplifier logger simplifier =
-    runSimplifier simplifier logger
+evalSimplifier logger (Simplifier simpl) =
+    withSolver' $ \solver ->
+        runReaderT simpl (Environment solver logger)
+
+-- * Implementation
 
 {-| Wraps a function that evaluates Kore functions on StepPatterns.
 -}
@@ -165,19 +352,17 @@ that it applies the substitution on the predicate.
 -}
 newtype PredicateSubstitutionSimplifier level =
     PredicateSubstitutionSimplifier
-        (forall variable
-        .   ( FreshVariable variable
-            , MetaOrObject level
-            , Ord (variable level)
-            , OrdMetaOrObject variable
-            , Show (variable level)
-            , ShowMetaOrObject variable
-            , Unparse (variable level)
-            , SortedVariable variable
-            )
-        => PredicateSubstitution level variable
-        -> Simplifier
-            ( PredicateSubstitution level variable
-            , SimplificationProof level
-            )
-        )
+        { getPredicateSubstitutionSimplifier
+            ::  forall variable
+            .   ( FreshVariable variable
+                , MetaOrObject level
+                , Ord (variable level)
+                , OrdMetaOrObject variable
+                , Show (variable level)
+                , ShowMetaOrObject variable
+                , Unparse (variable level)
+                , SortedVariable variable
+                )
+            => PredicateSubstitution level variable
+            -> BranchT Simplifier (PredicateSubstitution level variable)
+        }
diff --git a/kore/src/Kore/Step/Simplification/Predicate.hs b/kore/src/Kore/Step/Simplification/Predicate.hs
index b351970a80..7f32ee44c3 100644
--- a/kore/src/Kore/Step/Simplification/Predicate.hs
+++ b/kore/src/Kore/Step/Simplification/Predicate.hs
@@ -11,29 +11,25 @@ module Kore.Step.Simplification.Predicate
     ( simplifyPartial
     ) where
 
+import qualified Control.Monad.Trans as Monad.Trans
 import qualified Data.Text.Prettyprint.Doc as Pretty
 
-import           Kore.AST.Pure
-import           Kore.AST.Valid
-import           Kore.Predicate.Predicate
-                 ( Predicate, unwrapPredicate )
-import           Kore.Step.Representation.ExpandedPattern
-                 ( PredicateSubstitution, Predicated (..) )
-import qualified Kore.Step.Representation.ExpandedPattern as Predicated
-import qualified Kore.Step.Representation.MultiOr as MultiOr
-                 ( extractPatterns )
-import           Kore.Step.Simplification.Data
-                 ( PredicateSubstitutionSimplifier, SimplificationProof (..),
-                 Simplifier, StepPatternSimplifier (StepPatternSimplifier),
-                 StepPatternSimplifier )
-import           Kore.Unparser
-import           Kore.Variables.Fresh
-                 ( FreshVariable )
+import Kore.AST.Pure
+import Kore.AST.Valid
+import Kore.Predicate.Predicate
+       ( Predicate, unwrapPredicate )
+import Kore.Step.Representation.ExpandedPattern
+       ( PredicateSubstitution, Predicated (..) )
+import Kore.Step.Simplification.Data
+import Kore.Unparser
+import Kore.Variables.Fresh
+       ( FreshVariable )
 
-{-| Simplifies a predicate, producing another predicate and a substitution,
-without trying to reapply the substitution on the predicate.
+{- | Simplify the 'Predicate' once; return but do not apply the substitution.
+
+@simplifyPartial@ does not attempt to apply the resulting substitution and
+re-simplify the result; see "Kore.Step.Simplification.PredicateSubstitution".
 
-TODO(virgil): Make this fully simplify.
 -}
 simplifyPartial
     ::  ( FreshVariable variable
@@ -48,38 +44,23 @@ simplifyPartial
     => PredicateSubstitutionSimplifier level
     -> StepPatternSimplifier level
     -> Predicate level variable
-    -> Simplifier
-        ( PredicateSubstitution level variable
-        , SimplificationProof level
-        )
+    -> BranchT Simplifier (PredicateSubstitution level variable)
 simplifyPartial
     substitutionSimplifier
     (StepPatternSimplifier simplifier)
     predicate
   = do
     (patternOr, _proof) <-
-        simplifier substitutionSimplifier (unwrapPredicate predicate)
-    case MultiOr.extractPatterns patternOr of
-        [] -> return
-            ( Predicated.bottomPredicate
-            , SimplificationProof
-            )
-        [ Predicated
-                { term = Top_ _
-                , predicate = simplifiedPredicate
-                , substitution = simplifiedSubstitution
-                }
-            ] -> return
-                ( Predicated
-                    { term = ()
-                    , predicate = simplifiedPredicate
-                    , substitution = simplifiedSubstitution
-                    }
-                , SimplificationProof
-                )
-        [patt] ->
-            (error . show . Pretty.vsep)
-                [ "Expecting a top term!"
-                , unparse patt
-                ]
-        _ -> error ("Expecting at most one result " ++ show patternOr)
+        Monad.Trans.lift
+        $ simplifier substitutionSimplifier (unwrapPredicate predicate)
+    -- Despite using Monad.Trans.lift above, we do not need to explicitly check
+    -- for \bottom because patternOr is an OrOfExpandedPattern.
+    scatter (eraseTerm <$> patternOr)
+  where
+    eraseTerm predicated@Predicated { term }
+      | Top_ _ <- term = predicated { term = () }
+      | otherwise =
+        (error . show . Pretty.vsep)
+            [ "Expecting a \\top term, but found:"
+            , unparse predicated
+            ]
diff --git a/kore/src/Kore/Step/Simplification/PredicateSubstitution.hs b/kore/src/Kore/Step/Simplification/PredicateSubstitution.hs
index 120b788046..ae698d486c 100644
--- a/kore/src/Kore/Step/Simplification/PredicateSubstitution.hs
+++ b/kore/src/Kore/Step/Simplification/PredicateSubstitution.hs
@@ -12,8 +12,9 @@ module Kore.Step.Simplification.PredicateSubstitution
     , simplify
     ) where
 
-import Data.List
-       ( group )
+import qualified Control.Monad.Trans as Monad.Trans
+import           Data.List
+                 ( group )
 
 import           Kore.AST.Common
                  ( SortedVariable )
@@ -26,10 +27,7 @@ import           Kore.Step.Axiom.Data
 import           Kore.Step.Representation.ExpandedPattern
                  ( PredicateSubstitution, Predicated (..) )
 import           Kore.Step.Simplification.Data
-                 ( PredicateSubstitutionSimplifier (..),
-                 SimplificationProof (..), Simplifier, StepPatternSimplifier )
 import qualified Kore.Step.Simplification.Predicate as Predicate
-                 ( simplifyPartial )
 import           Kore.Step.StepperAttributes
                  ( StepperAttributes )
 import           Kore.Step.Substitution
@@ -50,11 +48,13 @@ create
     -> PredicateSubstitutionSimplifier level
 create tools simplifier axiomIdToSimplifier =
     PredicateSubstitutionSimplifier
-        (\p -> simplify tools simplifier axiomIdToSimplifier p 0)
+        (simplify tools simplifier axiomIdToSimplifier 0)
+
+{- | Simplify a 'PredicateSubstitution'.
+
+@simplify@ applies the substitution to the predicate and simplifies the
+result. The result is re-simplified once.
 
-{-| Simplifies a predicate-substitution by applying the substitution to the
-predicate, simplifying the result and repeating with the new
-substitution-predicate.
 -}
 simplify
     ::  ( MetaOrObject level
@@ -70,18 +70,15 @@ simplify
     -> StepPatternSimplifier level
     -> BuiltinAndAxiomSimplifierMap level
     -- ^ Map from axiom IDs to axiom evaluators
-    -> PredicateSubstitution level variable
     -> Int
-    -> Simplifier
-        ( PredicateSubstitution level variable
-        , SimplificationProof level
-        )
+    -> PredicateSubstitution level variable
+    -> BranchT Simplifier (PredicateSubstitution level variable)
 simplify
     tools
     simplifier
     axiomIdToSimplifier
-    initialValue@Predicated { predicate, substitution }
     times
+    initialValue@Predicated { predicate, substitution }
   = do
     let substitution' = Substitution.toMap substitution
         substitutedPredicate = Predicate.substitute substitution' predicate
@@ -90,28 +87,20 @@ simplify
     -- This was needed because, when we need to simplify 'requires' clauses,
     -- this needs to run more than once.
     if substitutedPredicate == predicate && times > 1
-        then return (initialValue, SimplificationProof)
+        then return initialValue
         else do
-            (   Predicated
-                    { predicate = simplifiedPredicate
-                    , substitution = simplifiedSubstitution
-                    }
-                , _proof
-                ) <-
-                    Predicate.simplifyPartial
-                        substitutionSimplifier
-                        simplifier
-                        substitutedPredicate
+            simplified <-
+                Predicate.simplifyPartial
+                    substitutionSimplifier
+                    simplifier
+                    substitutedPredicate
+
+            let Predicated { predicate = simplifiedPredicate } = simplified
+                Predicated { substitution = simplifiedSubstitution } =
+                    simplified
 
             if Substitution.null simplifiedSubstitution
-                then return
-                    ( Predicated
-                        { term = ()
-                        , predicate = simplifiedPredicate
-                        , substitution
-                        }
-                    , SimplificationProof
-                    )
+                then return simplified { substitution }
                 else do
                     -- TODO(virgil): Optimize. Since both substitution and
                     -- simplifiedSubstitution have distinct variables, it is
@@ -120,26 +109,28 @@ simplify
                     assertDistinctVariables
                         (substitution <> simplifiedSubstitution)
                     (mergedPredicateSubstitution, _proof) <-
-                        mergePredicatesAndSubstitutions
+                        Monad.Trans.lift
+                        $ mergePredicatesAndSubstitutions
                             tools
                             substitutionSimplifier
                             simplifier
                             axiomIdToSimplifier
                             [simplifiedPredicate]
                             [substitution, simplifiedSubstitution]
-                    return (mergedPredicateSubstitution, SimplificationProof)
+                    returnPruned mergedPredicateSubstitution
   where
     substitutionSimplifier =
         PredicateSubstitutionSimplifier
-            (\p -> simplify tools simplifier axiomIdToSimplifier p (times + 1))
+            (simplify tools simplifier axiomIdToSimplifier (times + 1))
 
 assertDistinctVariables
-    :: forall level variable
+    :: forall level variable m
     .   ( Show (variable level)
         , Eq (variable level)
+        , Monad m
         )
     => Substitution level variable
-    -> Simplifier ()
+    -> m ()
 assertDistinctVariables subst =
     case filter moreThanOne (group variables) of
         [] -> return ()
diff --git a/kore/src/Kore/Step/Substitution.hs b/kore/src/Kore/Step/Substitution.hs
index ab58c4ab38..07eb4d1ec4 100644
--- a/kore/src/Kore/Step/Substitution.hs
+++ b/kore/src/Kore/Step/Substitution.hs
@@ -20,11 +20,14 @@ module Kore.Step.Substitution
 
 import           Control.Monad.Except
                  ( ExceptT, lift, runExceptT, withExceptT )
+import qualified Control.Monad.Morph as Monad.Morph
 import           Control.Monad.Trans.Class
                  ( MonadTrans )
 import qualified Control.Monad.Trans.Class as Monad.Trans
-import           Data.Foldable
-                 ( fold )
+import qualified Control.Monad.Trans.Except as Except
+import qualified Data.Foldable as Foldable
+import           GHC.Stack
+                 ( HasCallStack )
 
 import           Kore.AST.Common
                  ( SortedVariable )
@@ -33,18 +36,13 @@ import           Kore.IndexedModule.MetadataTools
                  ( MetadataTools (..) )
 import           Kore.Predicate.Predicate
                  ( Predicate, makeAndPredicate, makeMultipleAndPredicate )
-import qualified Kore.Predicate.Predicate as Predicate
-                 ( isFalse )
 import           Kore.Step.Axiom.Data
                  ( BuiltinAndAxiomSimplifierMap )
 import           Kore.Step.Representation.ExpandedPattern
                  ( ExpandedPattern, PredicateSubstitution, Predicated (..),
                  substitutionToPredicate )
 import qualified Kore.Step.Representation.ExpandedPattern as ExpandedPattern
-                 ( bottom )
 import           Kore.Step.Simplification.Data
-                 ( PredicateSubstitutionSimplifier (..), Simplifier,
-                 StepPatternSimplifier )
 import           Kore.Step.StepperAttributes
 import           Kore.Unification.Data
                  ( UnificationProof (EmptyUnificationProof) )
@@ -83,7 +81,7 @@ normalize
     -> StepPatternSimplifier level
     -> BuiltinAndAxiomSimplifierMap level
     -> ExpandedPattern level variable
-    -> Simplifier ( ExpandedPattern level variable )
+    -> BranchT Simplifier (ExpandedPattern level variable)
 normalize
     tools
     substitutionSimplifier
@@ -91,28 +89,27 @@ normalize
     axiomIdToSimplifier
     Predicated { term, predicate, substitution }
   = do
-    x <- runExceptT $
-        normalizeSubstitutionAfterMerge
+    result <-
+        runExceptT
+        $ normalizeWorker
             tools
             substitutionSimplifier
             simplifier
             axiomIdToSimplifier
             Predicated { term = (), predicate, substitution }
-    return $ case x of
-      Right (Predicated { predicate = p, substitution = s }, _) ->
-          if Predicate.isFalse p
-              then ExpandedPattern.bottom
-              else Predicated term p s
-      Left _ ->
-          Predicated
-              { term
-              , predicate =
-                    makeAndPredicate predicate
-                    $ substitutionToPredicate substitution
-              , substitution = mempty
-              }
+    case result of
+        Right normal -> return normal { term }
+        Left _ ->
+            return Predicated
+                { term
+                , predicate =
+                    makeAndPredicate
+                        predicate
+                        (substitutionToPredicate substitution)
+                , substitution = mempty
+                }
 
-normalizeSubstitutionAfterMerge
+normalizeWorker
     ::  ( MetaOrObject level
         , Ord (variable level)
         , Show (variable level)
@@ -128,58 +125,54 @@ normalizeSubstitutionAfterMerge
     -> BuiltinAndAxiomSimplifierMap level
     -> PredicateSubstitution level variable
     -> ExceptT
-          ( UnificationOrSubstitutionError level variable )
-          Simplifier
-          ( PredicateSubstitution level variable
-          , UnificationProof level variable
-          )
-normalizeSubstitutionAfterMerge
+          (UnificationOrSubstitutionError level variable)
+          (BranchT Simplifier)
+          (PredicateSubstitution level variable)
+normalizeWorker
     tools
     wrappedSimplifier@(PredicateSubstitutionSimplifier substitutionSimplifier)
     simplifier
     axiomIdToSimplifier
     Predicated { predicate, substitution }
   = do
-    (Predicated
-            { predicate = duplicationPredicate
-            , substitution = duplicationSubstitution
-            }
-        , proof
-        ) <-
-            normalizeSubstitutionDuplication' substitution
-
-    Predicated
-        { predicate = normalizePredicate
-        , substitution = normalizedSubstitution
-        } <- normalizeSubstitution' duplicationSubstitution
+    duplication <- normalizeSubstitutionDuplication' substitution
+    let
+        Predicated { substitution = duplicationSubstitution } = duplication
+        Predicated { predicate = duplicationPredicate } = duplication
 
+    normalized <- normalizeSubstitution' duplicationSubstitution
     let
+        Predicated { substitution = normalizedSubstitution } = normalized
+        Predicated { predicate = normalizedPredicate } = normalized
+
         mergedPredicate =
             makeMultipleAndPredicate
-                [predicate, duplicationPredicate, normalizePredicate]
-
-    (resultPredicateSubstitution, _proof) <-
-        lift $ substitutionSimplifier
-            Predicated
-                { term = ()
-                , predicate = mergedPredicate
-                , substitution = normalizedSubstitution
-                }
+                [predicate, duplicationPredicate, normalizedPredicate]
 
-    return
-        ( resultPredicateSubstitution
-        , proof
-        )
+    lift $ substitutionSimplifier
+        Predicated
+            { term = ()
+            , predicate = mergedPredicate
+            , substitution = normalizedSubstitution
+            }
   where
-    normalizeSubstitutionDuplication' =
-        normalizeSubstitutionDuplication
-            tools
-            wrappedSimplifier
-            simplifier
-            axiomIdToSimplifier
-    normalizeSubstitution' =
-        withExceptT substitutionToUnifyOrSubError
-            . normalizeSubstitution tools
+    normalizeSubstitutionDuplication' substitution' = do
+        (duplication, _) <-
+            Monad.Morph.hoist lift
+            $ normalizeSubstitutionDuplication
+                tools
+                wrappedSimplifier
+                simplifier
+                axiomIdToSimplifier
+                substitution'
+        Monad.Trans.lift (returnPruned duplication)
+
+    normalizeSubstitution' substitution' = do
+        normalized <-
+            Monad.Morph.hoist lift
+            $ withExceptT substitutionToUnifyOrSubError
+            $ normalizeSubstitution tools substitution'
+        Monad.Trans.lift (returnPruned normalized)
 
 {-|'mergePredicatesAndSubstitutions' merges a list of substitutions into
 a single one, then merges the merge side condition and the given condition list
@@ -276,7 +269,7 @@ mergePredicatesAndSubstitutionsExcept
     substitutions
   = do
     let
-        mergedSubstitution = fold substitutions
+        mergedSubstitution = Foldable.fold substitutions
         mergedPredicate = makeMultipleAndPredicate predicates
     (Predicated {predicate, substitution}, _proof) <-
         normalizeSubstitutionAfterMerge
@@ -462,3 +455,49 @@ createLiftedPredicatesAndSubstitutionsMerger
             predicates
             substitutions
         return merged
+
+normalizeSubstitutionAfterMerge
+    ::  ( MetaOrObject level
+        , Ord (variable level)
+        , Show (variable level)
+        , Unparse (variable level)
+        , OrdMetaOrObject variable
+        , ShowMetaOrObject variable
+        , SortedVariable variable
+        , FreshVariable variable
+        , HasCallStack
+        )
+    => MetadataTools level StepperAttributes
+    -> PredicateSubstitutionSimplifier level
+    -> StepPatternSimplifier level
+    -> BuiltinAndAxiomSimplifierMap level
+    -> PredicateSubstitution level variable
+    -> ExceptT
+          ( UnificationOrSubstitutionError level variable )
+          Simplifier
+          ( PredicateSubstitution level variable
+          , UnificationProof level variable
+          )
+normalizeSubstitutionAfterMerge
+    tools
+    substitutionSimplifier
+    simplifier
+    axiomIdToSimplifier
+    predicateSubstitution
+  = do
+    results <-
+        lift $ getBranches $ runExceptT
+        $ normalizeWorker
+            tools
+            substitutionSimplifier
+            simplifier
+            axiomIdToSimplifier
+            predicateSubstitution
+    case results of
+        [] -> return
+            ( ExpandedPattern.bottomPredicate
+            , EmptyUnificationProof
+            )
+        [Right normal] -> return (normal, EmptyUnificationProof)
+        [Left e] -> Except.throwE e
+        _ -> error "Not implemented: branching during normalization"
diff --git a/kore/src/ListT.hs b/kore/src/ListT.hs
new file mode 100644
index 0000000000..cce1ed1301
--- /dev/null
+++ b/kore/src/ListT.hs
@@ -0,0 +1,131 @@
+{-|
+Module      : ListT
+Description : List monad transformer
+Copyright   : (c) Runtime Verification, 2019
+License     : NCSA
+Maintainer  : thomas.tuegel@runtimeverification.com
+
+This module implements the list monad transformer.
+
+-}
+
+module ListT
+    ( ListT (..)
+    , toListM
+    -- * Re-exports
+    , Alternative (..), MonadPlus (..)
+    ) where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.IO.Class
+import Control.Monad.RWS.Class
+import Control.Monad.Trans.Class
+import Data.Foldable
+import Data.Typeable
+
+{- | The list monad transformer written as a right-associative fold.
+
+Note that none of its basic instances—e.g. 'Functor', 'Applicative',
+'Alternative', 'Monad'—rely on the transformed type @m@ because @ListT@ takes
+those behaviors from the instances for lists.
+
+'empty' is related to the empty list:
+@
+toListM empty === return []
+@
+
+'pure' (or 'return') constructs singleton lists:
+@
+toListM (pure a) === return [a]
+@
+
+'<|>' fills the role of '<>' or '++':
+@
+toListM (pure a <|> pure b) === return [a, b]
+@
+
+If we think of '<|>' an addition, then '<*>' is multiplication, and distributes
+as such:
+@
+toListM ((pure f <|> pure g) <*> (pure a <|> pure b))
+===
+return [f a, f b, g a, g b]
+@
+
+ -}
+newtype ListT m a =
+    ListT { getListT :: forall r. (a -> m r -> m r) -> m r -> m r }
+    deriving (Typeable)
+
+instance Functor (ListT m) where
+    fmap f as = ListT $ \yield -> getListT as (yield . f)
+    {-# INLINE fmap #-}
+
+instance Applicative (ListT m) where
+    pure a = ListT $ \yield -> yield a
+    {-# INLINE pure #-}
+
+    (<*>) fs as =
+        ListT $ \yield ->
+            getListT fs $ \f ->
+                getListT as $ \a ->
+                    yield (f a)
+    {-# INLINE (<*>) #-}
+
+instance Alternative (ListT m) where
+    empty = ListT $ \_ next -> next
+    {-# INLINE empty #-}
+
+    (<|>) as bs = ListT $ \yield -> getListT as yield . getListT bs yield
+    {-# INLINE (<|>) #-}
+
+instance Monad (ListT m) where
+    return = pure
+    {-# INLINE return #-}
+
+    (>>=) as k =
+        ListT $ \yield ->
+            getListT as $ \a ->
+                getListT (k a) yield
+    {-# INLINE (>>=) #-}
+
+instance MonadPlus (ListT m)
+
+instance MonadTrans ListT where
+    lift m = ListT $ \yield next -> m >>= \a -> yield a next
+    {-# INLINE lift #-}
+
+instance MonadReader r m => MonadReader r (ListT m) where
+    ask = lift ask
+    {-# INLINE ask #-}
+
+    reader f = lift (reader f)
+    {-# INLINE reader #-}
+
+    local f as = ListT $ \yield -> local f . getListT as yield
+    {-# INLINE local #-}
+
+instance MonadState s m => MonadState s (ListT m) where
+    get = lift get
+    {-# INLINE get #-}
+
+    put s = lift (put s)
+    {-# INLINE put #-}
+
+    state f = lift (state f)
+    {-# INLINE state #-}
+
+instance MonadIO m => MonadIO (ListT m) where
+    liftIO = lift . liftIO
+    {-# INLINE liftIO #-}
+
+instance (Applicative f, Foldable f) => Foldable (ListT f) where
+    foldMap f as =
+        fold (getListT as (\a r -> mappend (f a) <$> r) (pure mempty))
+    {-# INLINE foldMap #-}
+
+{- | Collect all values produced by a @'ListT' m@ as a list in @m@.
+ -}
+toListM :: Applicative m => ListT m a -> m [a]
+toListM as = getListT as (\a mr -> (a :) <$> mr) (pure [])
diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs
index f77bf04aba..283326ad17 100644
--- a/kore/src/SMT.hs
+++ b/kore/src/SMT.hs
@@ -56,6 +56,8 @@ import qualified Control.Monad.Writer.Strict as Writer.Strict
 import           Data.Limit
 import           Data.Text
                  ( Text )
+
+import           ListT
 import           SimpleSMT
                  ( Result (..), SExpr (..), Solver )
 import qualified SimpleSMT
@@ -149,6 +151,9 @@ instance (MonadSMT m, Monoid w) => MonadSMT (Writer.Lazy.WriterT w m) where
 instance (MonadSMT m, Monoid w) => MonadSMT (Writer.Strict.WriterT w m) where
     liftSMT = Trans.lift . liftSMT
 
+instance MonadSMT m => MonadSMT (ListT m) where
+    liftSMT = Trans.lift . liftSMT
+
 {- | Initialize a new solver with the given 'Config'.
 
 The new solver is returned in an 'MVar' for thread-safety.
diff --git a/kore/test/Test/Kore/Builtin/Map.hs b/kore/test/Test/Kore/Builtin/Map.hs
index 7ff8c96e2f..5c1ec04139 100644
--- a/kore/test/Test/Kore/Builtin/Map.hs
+++ b/kore/test/Test/Kore/Builtin/Map.hs
@@ -522,6 +522,4 @@ mkIntVar variableName =
     mkVar Variable { variableName, variableCounter = mempty, variableSort = intSort }
 
 mockSubstitutionSimplifier :: PredicateSubstitutionSimplifier level
-mockSubstitutionSimplifier =
-    PredicateSubstitutionSimplifier
-        (\x -> return (x, SimplificationProof))
+mockSubstitutionSimplifier = PredicateSubstitutionSimplifier return
diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs
index b13f82444b..4bcdf6bf42 100644
--- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs
+++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs
@@ -583,9 +583,9 @@ test_andTermsSimplification =
                                 , (Mock.bConcrete, fOfB)
                                 ]
                         , predicate = makeTruePredicate
-                        , substitution = Substitution.unsafeWrap
-                            [ (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
-                            , (Mock.x, fOfA)
+                        , substitution = Substitution.wrap
+                            [ (Mock.x, fOfA)
+                            , (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
                             ]
                         }
             actual <-
@@ -611,9 +611,9 @@ test_andTermsSimplification =
                                 , (Mock.bConcrete, fOfB)
                                 ]
                         , predicate = makeTruePredicate
-                        , substitution = Substitution.unsafeWrap
-                            [ (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
-                            , (Mock.x, fOfA)
+                        , substitution = Substitution.wrap
+                            [ (Mock.x, fOfA)
+                            , (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
                             ]
                         }
             actual <-
@@ -639,9 +639,9 @@ test_andTermsSimplification =
                                 , (Mock.bConcrete, fOfB)
                                 ]
                         , predicate = makeTruePredicate
-                        , substitution = Substitution.unsafeWrap
-                            [ (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
-                            , (Mock.x, fOfA)
+                        , substitution = Substitution.wrap
+                            [ (Mock.x, fOfA)
+                            , (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
                             ]
                         }
             actual <-
@@ -667,9 +667,9 @@ test_andTermsSimplification =
                                 , (Mock.bConcrete, fOfB)
                                 ]
                         , predicate = makeTruePredicate
-                        , substitution = Substitution.unsafeWrap
-                            [ (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
-                            , (Mock.x, fOfA)
+                        , substitution = Substitution.wrap
+                            [ (Mock.x, fOfA)
+                            , (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
                             ]
                         }
             actual <-
diff --git a/kore/test/Test/Kore/Step/Simplification/Equals.hs b/kore/test/Test/Kore/Step/Simplification/Equals.hs
index aaa30ec3d2..db5f4180f1 100644
--- a/kore/test/Test/Kore/Step/Simplification/Equals.hs
+++ b/kore/test/Test/Kore/Step/Simplification/Equals.hs
@@ -693,9 +693,9 @@ test_equalsSimplification_Patterns =
                         makeAndPredicate
                             (makeCeilPredicate fOfA)
                             (makeCeilPredicate fOfB)
-                    , substitution = Substitution.unsafeWrap
-                        [ (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
-                        , (Mock.x, fOfA)
+                    , substitution = Substitution.wrap
+                        [ (Mock.x, fOfA)
+                        , (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
                         ]
                     }
                 (Mock.builtinMap
@@ -717,9 +717,9 @@ test_equalsSimplification_Patterns =
                         makeAndPredicate
                             (makeCeilPredicate fOfA)
                             (makeCeilPredicate fOfB)
-                    , substitution = Substitution.unsafeWrap
-                        [ (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
-                        , (Mock.x, fOfA)
+                    , substitution = Substitution.wrap
+                        [ (Mock.x, fOfA)
+                        , (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
                         ]
                     }
                 (Mock.builtinMap
@@ -741,9 +741,9 @@ test_equalsSimplification_Patterns =
                         makeAndPredicate
                             (makeCeilPredicate fOfA)
                             (makeCeilPredicate fOfB)
-                    , substitution = Substitution.unsafeWrap
-                        [ (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
-                        , (Mock.x, fOfA)
+                    , substitution = Substitution.wrap
+                        [ (Mock.x, fOfA)
+                        , (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
                         ]
                     }
                 (Mock.concatMap
@@ -765,9 +765,9 @@ test_equalsSimplification_Patterns =
                         makeAndPredicate
                             (makeCeilPredicate fOfA)
                             (makeCeilPredicate fOfB)
-                    , substitution = Substitution.unsafeWrap
-                        [ (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
-                        , (Mock.x, fOfA)
+                    , substitution = Substitution.wrap
+                        [ (Mock.x, fOfA)
+                        , (Mock.m, Mock.builtinMap [(Mock.bConcrete, fOfB)])
                         ]
                     }
                 (Mock.concatMap
diff --git a/kore/test/Test/Kore/Step/Simplification/PredicateSubstitution.hs b/kore/test/Test/Kore/Step/Simplification/PredicateSubstitution.hs
index 5dbd1144bd..9ece6cd789 100644
--- a/kore/test/Test/Kore/Step/Simplification/PredicateSubstitution.hs
+++ b/kore/test/Test/Kore/Step/Simplification/PredicateSubstitution.hs
@@ -26,10 +26,8 @@ import           Kore.Step.Representation.ExpandedPattern
 import qualified Kore.Step.Representation.ExpandedPattern as Predicated
 import qualified Kore.Step.Representation.MultiOr as MultiOr
                  ( make )
-import           Kore.Step.Simplification.Data
-                 ( PredicateSubstitutionSimplifier (..),
-                 SimplificationProof (SimplificationProof), Simplifier,
-                 evalSimplifier )
+import           Kore.Step.Simplification.Data hiding
+                 ( runSimplifier )
 import qualified Kore.Step.Simplification.PredicateSubstitution as PSSimplifier
                  ( create )
 import qualified Kore.Step.Simplification.Simplifier as Simplifier
@@ -53,11 +51,11 @@ test_predicateSubstitutionSimplification =
     [ testCase "Identity for top and bottom" $ do
         actualBottom <- runSimplifier Map.empty Predicated.bottomPredicate
         assertEqualWithExplanation ""
-            Predicated.bottomPredicate
+            []
             actualBottom
         actualTop <- runSimplifier Map.empty Predicated.topPredicate
         assertEqualWithExplanation ""
-            Predicated.topPredicate
+            [Predicated.topPredicate]
             actualTop
 
     , testCase "Applies substitution to predicate" $ do
@@ -86,7 +84,7 @@ test_predicateSubstitutionSimplification =
                         , (Mock.y, Mock.b)
                         ]
                     }
-        assertEqualWithExplanation "" expect actual
+        assertEqualWithExplanation "" [expect] actual
 
     , testCase "Simplifies predicate after substitution" $ do
         let expect =
@@ -114,7 +112,7 @@ test_predicateSubstitutionSimplification =
                         , (Mock.y, Mock.functional01)
                         ]
                     }
-        assertEqualWithExplanation "" expect actual
+        assertEqualWithExplanation "" [expect] actual
 
     , testCase "Simplifies predicate after substitution" $ do
         let expect =
@@ -152,7 +150,7 @@ test_predicateSubstitutionSimplification =
                         , (Mock.y, Mock.functional01)
                         ]
                     }
-        assertEqualWithExplanation "" expect actual
+        assertEqualWithExplanation "" [expect] actual
 
     , testCase "Merges substitution from predicate simplification" $ do
         let expect =
@@ -186,7 +184,7 @@ test_predicateSubstitutionSimplification =
                         [ (Mock.y, Mock.b)
                         ]
                     }
-        assertEqualWithExplanation "" expect actual
+        assertEqualWithExplanation "" [expect] actual
 
     , testCase "Reapplies substitution from predicate simplification" $ do
         let expect =
@@ -229,7 +227,7 @@ test_predicateSubstitutionSimplification =
                         [ (Mock.y, Mock.b)
                         ]
                     }
-        assertEqualWithExplanation "" expect actual
+        assertEqualWithExplanation "" [expect] actual
 
     , testCase "Simplifies after reapplying substitution" $ do
         let expect =
@@ -273,7 +271,7 @@ test_predicateSubstitutionSimplification =
                         [ (Mock.y, Mock.b)
                         ]
                     }
-        assertEqualWithExplanation "" expect actual
+        assertEqualWithExplanation "" [expect] actual
     ]
 
 mockMetadataTools :: MetadataTools Object StepperAttributes
@@ -287,16 +285,14 @@ mockMetadataTools =
 runSimplifier
     :: BuiltinAndAxiomSimplifierMap Object
     -> CommonPredicateSubstitution Object
-    -> IO (CommonPredicateSubstitution Object)
+    -> IO [CommonPredicateSubstitution Object]
 runSimplifier patternSimplifierMap predicateSubstitution =
-    case simplifier of
-        (PredicateSubstitutionSimplifier unwrapped) ->
-            (<$>) fst
-            $ SMT.runSMT SMT.defaultConfig
-            $ evalSimplifier emptyLogger
-            $ unwrapped predicateSubstitution
+    SMT.runSMT SMT.defaultConfig
+    $ evalSimplifier emptyLogger
+    $ getBranches
+    $ simplifier predicateSubstitution
   where
-    simplifier =
+    PredicateSubstitutionSimplifier simplifier =
         PSSimplifier.create
             mockMetadataTools
             (Simplifier.create mockMetadataTools patternSimplifierMap)
diff --git a/kore/test/Test/ListT.hs b/kore/test/Test/ListT.hs
new file mode 100644
index 0000000000..db4b503154
--- /dev/null
+++ b/kore/test/Test/ListT.hs
@@ -0,0 +1,116 @@
+module Test.ListT where
+
+import           Hedgehog
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+
+import qualified Data.Foldable as Foldable
+import qualified Data.Function as Function
+import           Data.Functor.Identity
+
+import ListT
+
+genList :: Gen a -> Gen (ListT Identity a)
+genList genItem =
+    Foldable.asum . map pure <$> Gen.list (Range.linear 0 32) genItem
+
+genInteger :: Gen Integer
+genInteger = Gen.integral (Range.linear (-1024) 1024)
+
+genListInteger :: Gen (ListT Identity Integer)
+genListInteger = genList genInteger
+
+double :: Integer -> Integer
+double x = x + x
+
+square :: Integer -> Integer
+square x = x * x
+
+showListT :: Show a => ListT Identity a -> String
+showListT = show . toList . fmap show
+
+toList :: ListT Identity a -> [a]
+toList = Foldable.toList
+
+onList :: ([a] -> [a] -> r) -> ListT Identity a -> ListT Identity a -> r
+onList f = Function.on f toList
+
+hprop_FunctorIdentity :: Property
+hprop_FunctorIdentity = property $ do
+    xs <- forAllWith showListT genListInteger
+    onList (===) (id xs) (fmap id xs)
+
+hprop_FunctorComposition :: Property
+hprop_FunctorComposition = property $ do
+    xs <- forAllWith showListT genListInteger
+    onList (===)
+        (fmap (double . square)      xs)
+        ((fmap double . fmap square) xs)
+
+hprop_ApplicativeIdentity :: Property
+hprop_ApplicativeIdentity = property $ do
+    v <- forAllWith showListT genListInteger
+    onList (===) v (pure id <*> v)
+
+hprop_ApplicativeComposition :: Property
+hprop_ApplicativeComposition = property $ do
+    u <- fmap (+) <$> forAllWith showListT genListInteger
+    v <- fmap (*) <$> forAllWith showListT genListInteger
+    w <- forAllWith showListT genListInteger
+    onList (===)
+        (pure (.) <*> u <*> v <*> w)
+        (u <*> (v <*> w))
+
+hprop_ApplicativeHomomorphism :: Property
+hprop_ApplicativeHomomorphism = property $ do
+    x <- forAll genInteger
+    onList (===)
+        (pure double <*> pure x)
+        (pure (double x))
+    onList (===)
+        (pure square <*> pure x)
+        (pure (square x))
+
+hprop_ApplicativeInterchange :: Property
+hprop_ApplicativeInterchange = property $ do
+    u <- fmap (+) <$> forAllWith showListT genListInteger
+    y <- forAll genInteger
+    onList (===)
+        (u <*> pure y)
+        (pure ($ y) <*> u)
+
+hprop_AlternativeIdentity :: Property
+hprop_AlternativeIdentity = property $ do
+    u <- forAllWith showListT genListInteger
+    onList (===) u (empty <|> u)
+    onList (===) u (u <|> empty)
+
+hprop_AlternativeAnnihilator :: Property
+hprop_AlternativeAnnihilator = property $ do
+    u <- fmap (+) <$> forAllWith showListT genListInteger
+    onList (===) empty (u <*> empty)
+
+hprop_AlternativeAssociative :: Property
+hprop_AlternativeAssociative = property $ do
+    xs <- forAllWith showListT genListInteger
+    ys <- forAllWith showListT genListInteger
+    zs <- forAllWith showListT genListInteger
+    onList (===) ((xs <|> ys) <|> zs) (xs <|> (ys <|> zs))
+
+hprop_MonadLeftUnit :: Property
+hprop_MonadLeftUnit = property $ do
+    k <- (\xs y -> fmap (+ y) xs) <$> forAllWith showListT genListInteger
+    a <- forAll genInteger
+    onList (===) (k a) (return a >>= k)
+
+hprop_MonadRightUnit :: Property
+hprop_MonadRightUnit = property $ do
+    m <- forAllWith showListT genListInteger
+    onList (===) m (m >>= return)
+
+hprop_MonadAssociative :: Property
+hprop_MonadAssociative = property $ do
+    k <- (\xs y -> fmap (+ y) xs) <$> forAllWith showListT genListInteger
+    h <- (\xs y -> fmap (+ y) xs) <$> forAllWith showListT genListInteger
+    m <- forAllWith showListT genListInteger
+    onList (===) (m >>= (\x -> k x >>= h)) ((m >>= k) >>= h)