diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG
index 03facaf36..e1e61aa21 100644
--- a/copilot-theorem/CHANGELOG
+++ b/copilot-theorem/CHANGELOG
@@ -1,3 +1,5 @@
+2026-07-03
+        * Remove use of LambdaCase (#736)
 2026-05-07
         * Version bump (4.7.1). (#730)
         * Handle special Float values correctly for counterexamples. (#697)
diff --git a/copilot-theorem/src/Copilot/Theorem/IL/Spec.hs b/copilot-theorem/src/Copilot/Theorem/IL/Spec.hs
index 62ed692bd..c33a44aea 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Spec.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Spec.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs                     #-}
-{-# LANGUAGE LambdaCase                #-}
 {-# LANGUAGE Safe                      #-}
 
 -- | This module implements the specification language for the IL format, an
@@ -51,7 +50,7 @@ data Type = Bool  | Real
   deriving (Eq, Ord)
 
 instance Show Type where
-  show = \case
+  show = \t -> case t of
     Bool  -> "Bool"
     Real  -> "Real"
     SBV8  -> "SBV8"
diff --git a/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs b/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
index 4bdaa47f3..e877e82e7 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Transform.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE Safe       #-}
 
 -- | Simplify IL expressions by partly evaluating operations on booleans.
@@ -15,7 +14,7 @@ import Copilot.Theorem.IL.Spec
 bsimpl :: Expr -> Expr
 bsimpl = until (\x -> bsimpl' x == x) bsimpl'
   where
-    bsimpl' = \case
+    bsimpl' = \expr -> case expr of
       Ite _ (ConstB True) e _     -> bsimpl' e
       Ite _ (ConstB False) _ e    -> bsimpl' e
       Ite t c e1 e2               -> Ite t (bsimpl' c) (bsimpl' e1) (bsimpl' e2)
diff --git a/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs b/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
index c1a6606ba..283c8dd53 100644
--- a/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE GADTs               #-}
-{-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE NamedFieldPuns      #-}
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE Safe                #-}
@@ -212,7 +211,7 @@ trConst t v = case t of
       | otherwise = Op1 t Neg $ ConstI t $ negate $ toInteger v
 
 trOp1 :: C.Op1 a b -> (Op1, Type)
-trOp1 = \case
+trOp1 = \op -> case op of 
   C.Not     -> (Not, Bool)
   C.Abs t   -> (Abs, trType t)
   -- C.Sign t  ->
@@ -237,7 +236,7 @@ trOp1 = \case
   _ -> error "Unsupported unary operator in input."
 
 trOp2 :: C.Op2 a b c -> (Op2, Type)
-trOp2 = \case
+trOp2 = \op -> case op of
   C.And          -> (And, Bool)
   C.Or           -> (Or, Bool)
 
@@ -270,7 +269,7 @@ trOp2 = \case
   _ -> error "Unsupported binary operator in input."
 
 trType :: C.Type a -> Type
-trType = \case
+trType = \op -> case op of
   C.Bool   -> Bool
   C.Int8   -> SBV8
   C.Int16  -> SBV16
diff --git a/copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs b/copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs
index e5661a748..49244fa59 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs             #-}
-{-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE NamedFieldPuns    #-}
 {-# LANGUAGE RankNTypes        #-}
 {-# LANGUAGE Trustworthy       #-}
@@ -329,7 +328,7 @@ getVars :: [Expr] -> [VarDescr]
 getVars = nubBy' (compare `on` varName) . concatMap getVars'
   where
     getVars' :: Expr -> [VarDescr]
-    getVars' = \case
+    getVars' = \v -> case v of
       ConstB _             -> []
       ConstI _ _           -> []
       ConstR _             -> []
@@ -370,12 +369,12 @@ kInduction' startK maxK s as ps = (fromMaybe (Output P.Unknown ["proof by k-indu
                     ++ [evalAt (_n_plus i) m | m <- toCheck, i <- [0 .. k]]
           stepInv = [evalAt (_n_plus $ k + 1) m | m <- toCheck]
 
-      entailment Base (modelInit ++ base) baseInv >>= \case
+      entailment Base (modelInit ++ base) baseInv >>= \res -> case res of
         Sat     -> invalid $ "base case failed for " ++ proofKind k
         Unknown -> unknown
         Unsat   ->
           if not inductive then valid ("proved without induction")
-          else entailment Step step stepInv >>= \case
+          else entailment Step step stepInv >>= \stepRes -> case stepRes of
             Sat     -> unknown
             Unknown -> unknown
             Unsat   -> valid $ "proved with " ++ proofKind k
@@ -391,7 +390,7 @@ onlySat' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s
 
       if inductive
         then unknown' "proposition requires induction to prove."
-        else entailment Base (modelInit ++ base) (map (Op1 Bool Not) baseInv) >>= \case
+        else entailment Base (modelInit ++ base) (map (Op1 Bool Not) baseInv) >>= \res -> case res of
           Unsat   -> invalid "prop not satisfiable"
           Unknown -> unknown' "failed to find a satisfying model"
           Sat     -> sat "prop is satisfiable"
@@ -407,7 +406,7 @@ onlyValidity' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s
 
       if inductive
         then unknown' "proposition requires induction to prove."
-        else entailment Base (modelInit ++ base) baseInv >>= \case
+        else entailment Base (modelInit ++ base) baseInv >>= \res -> case res of
           Unsat   -> valid "proof by SMT solver"
           Unknown -> unknown
           Sat     -> invalid "SMT solver found a counter-example."
diff --git a/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs b/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
index e179409e8..52d7a5d53 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE GADTs      #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE Safe       #-}
 
 -- | A backend to <http://www.tptp.org/ TPTP>, enabling to produce assertions
@@ -46,7 +45,7 @@ interpret str
   | otherwise                                   = Nothing
 
 expr :: Expr -> TptpExpr
-expr = \case
+expr = \e -> case e of
   ConstB v        -> Atom $ if v then "$true" else "$false"
   ConstR v        -> Atom $ show v
   ConstI _ v      -> Atom $ show v
@@ -67,7 +66,7 @@ expr = \case
                        Var off -> Atom $ f ++ "_n" ++ show off
 
 showOp1 :: Op1 -> String
-showOp1 = \case
+showOp1 = \op -> case op of
   Not   -> "~"
   Neg   -> "-"
   Abs   -> "abs"
@@ -88,7 +87,7 @@ showOp1 = \case
   Acosh -> "arccosh"
 
 showOp2 :: Op2 -> String
-showOp2 = \case
+showOp2 = \op -> case op of
   Eq    -> "="
   Le    -> "<="
   Lt    -> "<"
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
index dd95d45db..fbdca3ae3 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs                     #-}
-{-# LANGUAGE LambdaCase                #-}
 {-# LANGUAGE RankNTypes                #-}
 {-# LANGUAGE Safe                      #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
@@ -305,7 +304,7 @@ handleOp2 resT (op, e1, e2) handleExpr notHandledF mkOp notOp = case op of
     numComp ::
       C.Type cta ->
       (forall num . (Num num) => Op2 num Bool) -> m (expr resT)
-    numComp ta op = casting ta $ \case
+    numComp ta op = casting ta $ \t -> case t of
       Integer -> do
         e1' <- handleExpr Integer e1
         e2' <- handleExpr Integer e2
diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs
index 97e55a852..dc65b6c89 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4.hs
@@ -2,7 +2,6 @@
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE PatternSynonyms     #-}
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -414,21 +413,21 @@ proveInternal solver spec k = do
         let k' = k base_cases ind_case st
         satRes <-
           case solver of
-            CVC4 -> liftIO $ WS.runCVC4InOverride sym WS.defaultLogData clauses $ \case
+            CVC4 -> liftIO $ WS.runCVC4InOverride sym WS.defaultLogData clauses $ \res -> case res of
               WS.Sat (ge, _) -> k' (WS.Sat ge)
               WS.Unsat x -> k' (WS.Unsat x)
               WS.Unknown -> k' WS.Unknown
-            DReal -> liftIO $ WS.runDRealInOverride sym WS.defaultLogData clauses $ \case
+            DReal -> liftIO $ WS.runDRealInOverride sym WS.defaultLogData clauses $ \res -> case res of
               WS.Sat (c, m) -> do
                 ge <- WS.getAvgBindings c m
                 k' (WS.Sat ge)
               WS.Unsat x -> k' (WS.Unsat x)
               WS.Unknown -> k' WS.Unknown
-            Yices -> liftIO $ WS.runYicesInOverride sym WS.defaultLogData clauses $ \case
+            Yices -> liftIO $ WS.runYicesInOverride sym WS.defaultLogData clauses $ \res -> case res of
               WS.Sat ge -> k' (WS.Sat ge)
               WS.Unsat x -> k' (WS.Unsat x)
               WS.Unknown -> k' WS.Unknown
-            Z3 -> liftIO $ WS.runZ3InOverride sym WS.defaultLogData clauses $ \case
+            Z3 -> liftIO $ WS.runZ3InOverride sym WS.defaultLogData clauses $ \res -> case res of
               WS.Sat (ge, _) -> k' (WS.Sat ge)
               WS.Unsat x -> k' (WS.Unsat x)
               WS.Unknown -> k' WS.Unknown