diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -6,6 +6,13 @@
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.5.7 — 2023-09-21
+
+This version contains two fixes (see [#88](https://github.com/rzk-lang/rzk/pull/88)) for issues discovered in [rzk-lang/sHoTT#30](https://github.com/rzk-lang/sHoTT/pull/30#issuecomment-1729212862):
+
+1. We now only generate well-typed LEM instances in the tope solver, speeding up significantly.
+2. We fix $\eta$-rule for product cubes, to not get stopped by reflexive equality topes like $\langle \langle \pi_1 (t_{12}), \pi_2 (t_{12}) \rangle, t_3 \rangle \equiv \langle t_{12}, t_3 \rangle$.
+
 ## v0.5.6 — 2023-09-19
 
 This version fixes the behaviour of glob (see [`77b7cc0`](https://github.com/rzk-lang/rzk/commit/77b7cc0494fe0bfd1c9f1aa83db20f42cfda5794)).
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.5.6
+version:        0.5.7
 synopsis:       An experimental proof assistant for synthetic ∞-categories
 description:    Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 category:       Dependent Types
diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs
--- a/src/Rzk/TypeCheck.hs
+++ b/src/Rzk/TypeCheck.hs
@@ -865,10 +865,30 @@
 entail :: Eq var => [TermT var] -> TermT var -> Bool
 entail topes tope = all (`solveRHS` tope) $
   saturateTopes (allTopePoints tope) <$>
-    simplifyLHS topes'
+    simplifyLHSwithDisjunctions topes'
   where
     topes' = nubTermT (topes <> generateTopesForPoints (allTopePoints tope))
 
+entailM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool
+entailM topes tope = do
+  genTopes <- generateTopesForPointsM (allTopePoints tope)
+  let topes'    = nubTermT (topes <> genTopes)
+      topes''   = simplifyLHSwithDisjunctions topes'
+      topes'''  = saturateTopes (allTopePoints tope) <$> topes''
+  -- prettyTopes <- mapM ppTermInContext (saturateTopes (allTopePoints tope) (simplifyLHS topes'))
+  -- prettyTope <- ppTermInContext =<< nfTope tope
+  return $
+    -- trace ("entail " <> intercalate ", " prettyTopes <> " |- " <> prettyTope) $
+      all (`solveRHS` tope) topes'''
+
+entailTraceM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool
+entailTraceM topes tope = do
+  topes' <- mapM ppTermInContext topes
+  tope' <- ppTermInContext tope
+  result <- trace ("entail " <> intercalate ", " topes' <> " |- " <> tope') $
+        topes `entailM` tope
+  return $ trace ("  " <> show result) result
+
 nubTermT :: Eq var => [TermT var] -> [TermT var]
 nubTermT []     = []
 nubTermT (t:ts) = t : nubTermT (filter (/= t) ts)
@@ -896,6 +916,7 @@
 generateTopes newTopes oldTopes
   | topeBottomT `elem` newTopes = []
   | topeEQT cube2_0T cube2_1T `elem` newTopes = [topeBottomT]
+  | length oldTopes > 100 = []    -- FIXME
   | otherwise = concat
       [  -- symmetry EQ
         [ topeEQT y x | TopeEQT _ty x y <- newTopes ]
@@ -965,12 +986,27 @@
 generateTopesForPoints :: Eq var => [TermT var] -> [TermT var]
 generateTopesForPoints points = nubTermT $ concat
   [ [ topeOrT (topeLEQT x y) (topeLEQT y x)
-    | x : points' <- tails points, y <- points'
-    , x /= y
-    , x `notElem` [cube2_0T, cube2_1T]
-    , y `notElem` [cube2_0T, cube2_1T] ]
+    | x : points' <- tails (filter (`notElem` [cube2_0T, cube2_1T]) points)
+    , y <- points'
+    , x /= y ]
   ]
 
+generateTopesForPointsM :: Eq var => [TermT var] -> TypeCheck var [TermT var]
+generateTopesForPointsM points = do
+  let pairs = nub $ concat
+        [ [ (x, y)
+          | x : points' <- tails (filter (`notElem` [cube2_0T, cube2_1T]) points)
+          , y <- points'
+          , x /= y ]
+        ]
+  topes <- forM pairs $ \(x, y) -> do
+    xType <- typeOf x
+    yType <- typeOf y
+    return $ if (xType == cube2T) && (yType == cube2T)
+      then [topeOrT (topeLEQT x y) (topeLEQT y x)]
+      else []
+  return (concat topes)
+
 allTopePoints :: Eq var => TermT var -> [TermT var]
 allTopePoints = nubTermT . foldMap subPoints . nubTermT . topePoints
 
@@ -992,17 +1028,37 @@
     | Cube2T{} <- infoType -> [p]
   _ -> []
 
-simplifyLHS :: Eq var => [TermT var] -> [[TermT var]]
-simplifyLHS topes = map nubTermT $
+-- | Simplify the context, including disjunctions. See also 'simplifyLHS'.
+simplifyLHSwithDisjunctions :: Eq var => [TermT var] -> [[TermT var]]
+simplifyLHSwithDisjunctions topes = map nubTermT $
   case topes of
     [] -> [[]]
-    TopeTopT{} : topes' -> simplifyLHS topes'
+    TopeTopT{} : topes' -> simplifyLHSwithDisjunctions topes'
     TopeBottomT{} : _  -> [[topeBottomT]]
+    TopeAndT _ l r : topes' -> simplifyLHSwithDisjunctions (l : r : topes')
+
+    -- NOTE: it is inefficient to expand disjunctions immediately
+    TopeOrT  _ l r : topes' -> simplifyLHSwithDisjunctions (l : topes') <> simplifyLHSwithDisjunctions (r : topes')
+
+    TopeEQT  _ (PairT _ x y) (PairT _ x' y') : topes' ->
+      simplifyLHSwithDisjunctions (topeEQT x x' : topeEQT y y' : topes')
+    t : topes' -> map (t :) (simplifyLHSwithDisjunctions topes')
+
+-- | Simplify the context, except disjunctions. See also 'simplifyLHSwithDisjunctions'.
+simplifyLHS :: Eq var => [TermT var] -> [TermT var]
+simplifyLHS topes = nubTermT $
+  case topes of
+    [] -> []
+    TopeTopT{} : topes' -> simplifyLHS topes'
+    TopeBottomT{} : _  -> [topeBottomT]
     TopeAndT _ l r : topes' -> simplifyLHS (l : r : topes')
-    TopeOrT  _ l r : topes' -> simplifyLHS (l : topes') <> simplifyLHS (r : topes')
+
+    -- NOTE: it is inefficient to expand disjunctions immediately
+    -- TopeOrT  _ l r : topes' -> simplifyLHS (l : topes') <> simplifyLHS (r : topes')
+
     TopeEQT  _ (PairT _ x y) (PairT _ x' y') : topes' ->
       simplifyLHS (topeEQT x x' : topeEQT y y' : topes')
-    t : topes' -> map (t:) (simplifyLHS topes')
+    t : topes' -> t : simplifyLHS topes'
 
 solveRHS :: Eq var => [TermT var] -> TermT var -> Bool
 solveRHS topes tope =
@@ -1011,6 +1067,10 @@
     TopeTopT{}     -> True
     TopeEQT  _ty (PairT _ty1 x y) (PairT _ty2 x' y')
       | solveRHS topes (topeEQT x x') && solveRHS topes (topeEQT y y') -> True
+    TopeEQT  _ty (PairT TypeInfo{ infoType = CubeProductT _ cubeI cubeJ } x y) r
+      | solveRHS topes (topeEQT x (firstT cubeI r)) && solveRHS topes (topeEQT y (secondT cubeJ r)) -> True
+    TopeEQT  _ty l (PairT TypeInfo{ infoType = CubeProductT _ cubeI cubeJ } x y)
+      | solveRHS topes (topeEQT (firstT cubeI l) x) && solveRHS topes (topeEQT (secondT cubeJ l) y) -> True
     TopeEQT  _ty l r -> or
       [ l == r
       , tope `elem` topes
@@ -1032,7 +1092,7 @@
   performing (ActionContextEntails ctxTopes tope) $ do
     topes' <- asks localTopesNF
     tope' <- nfTope tope
-    return (topes' `entail` tope')
+    topes' `entailM` tope'
 
 checkTopeEntails :: Eq var => TermT var -> TypeCheck var Bool
 checkTopeEntails tope = do
@@ -1041,13 +1101,13 @@
     contextTopes <- asks localTopesNF
     restrictionTope <- nfTope tope
     let contextTopesRHS = foldr topeAndT topeTopT contextTopes
-    return ([restrictionTope] `entail` contextTopesRHS)
+    [restrictionTope] `entailM` contextTopesRHS
 
 checkEntails :: Eq var => TermT var -> TermT var -> TypeCheck var Bool
 checkEntails l r = do  -- FIXME: add action
   l' <- nfTope l
   r' <- nfTope r
-  return ([l'] `entail` r')
+  [l'] `entailM` r'
 
 contextEntailedBy :: Eq var => TermT var -> TypeCheck var ()
 contextEntailedBy tope = do
@@ -1056,8 +1116,9 @@
     contextTopes <- asks localTopesNF
     restrictionTope <- nfTope tope
     let contextTopesRHS = foldr topeOrT topeBottomT contextTopes
-    unless ([restrictionTope] `entail` contextTopesRHS) $
-      issueTypeError $ TypeErrorTopeNotSatisfied [restrictionTope] contextTopesRHS
+    [restrictionTope] `entailM` contextTopesRHS >>= \case
+      False -> issueTypeError $ TypeErrorTopeNotSatisfied [restrictionTope] contextTopesRHS
+      True -> return ()
 
 contextEntails :: Eq var => TermT var -> TypeCheck var ()
 contextEntails tope = do
@@ -1072,7 +1133,9 @@
 topesEquiv expected actual = performing (ActionUnifyTerms expected actual) $ do
   expected' <- nfT expected
   actual' <- nfT actual
-  return ([expected'] `entail` actual' && [actual'] `entail` expected')
+  (&&)
+    <$> [expected'] `entailM` actual'
+    <*> [actual'] `entailM` expected'
 
 contextEquiv :: Eq var => [TermT var] -> TypeCheck var ()
 contextEquiv topes = do
@@ -1082,10 +1145,12 @@
     recTopes <- mapM nfTope topes
     let contextTopesRHS = foldr topeOrT topeBottomT contextTopes
         recTopesRHS     = foldr topeOrT topeBottomT recTopes
-    unless (contextTopes `entail` recTopesRHS) $
-      issueTypeError $ TypeErrorTopeNotSatisfied contextTopes recTopesRHS
-    unless (recTopes `entail` contextTopesRHS) $
-      issueTypeError $ TypeErrorTopeNotSatisfied recTopes contextTopesRHS
+    contextTopes `entailM` recTopesRHS >>= \case
+      False -> issueTypeError $ TypeErrorTopeNotSatisfied contextTopes recTopesRHS
+      True -> return ()
+    recTopes `entailM` contextTopesRHS >>= \case
+      False -> issueTypeError $ TypeErrorTopeNotSatisfied recTopes contextTopesRHS
+      True -> return ()
 
 switchVariance :: TypeCheck var a -> TypeCheck var a
 switchVariance = local $ \Context{..} -> Context
@@ -1352,7 +1417,7 @@
 nfTope tt = performing (ActionNF tt) $ fmap termIsNF $ case tt of
   Pure var ->
     valueOfVar var >>= \case
-      Nothing   -> pure tt
+      Nothing   -> return tt
       Just term -> nfTope term
 
   -- see if normal form is already available
@@ -1592,9 +1657,9 @@
 
 unifyTopes :: Eq var => TermT var -> TermT var -> TypeCheck var ()
 unifyTopes l r = do
-  let equiv = and
-        [ [l] `entail` r
-        , [r] `entail` l ]
+  equiv <- (&&)
+    <$> [l] `entailM` r
+    <*> [r] `entailM` l
   unless equiv $
     issueTypeError (TypeErrorTopesNotEquivalent l r)
 
@@ -1850,7 +1915,7 @@
       , localTopesNF = tope' : localTopesNF
       , localTopesNFUnion = map nubTermT
           [ new <> old
-          | new <- simplifyLHS [tope']
+          | new <- simplifyLHSwithDisjunctions [tope']
           , old <- localTopesNFUnion ]
       , localTopesEntailBottom = entailsBottom
       , .. }
@@ -2714,7 +2779,7 @@
         . map (foldr topeAndT topeTopT)
         . map (filter (\tope -> all (`notElem` tope) sub))
         . map (saturateTopes [])
-        . simplifyLHS
+        . simplifyLHSwithDisjunctions
   contextTopes  <- asks (reduceContext . localTopesNF)
   contextTopes' <- localTope (componentWiseEQT dim (Pure super) x) $ asks (reduceContext . localTopesNF)
   forM (subTopes2 dim (Pure super)) $ \(shapeId, tope) -> do