diff --git a/kore/src/Kore/Simplify/Predicate.hs b/kore/src/Kore/Simplify/Predicate.hs
index f821d63259..73b35d72b6 100644
--- a/kore/src/Kore/Simplify/Predicate.hs
+++ b/kore/src/Kore/Simplify/Predicate.hs
@@ -56,6 +56,7 @@ import Kore.Rewrite.RewritingVariable (
     RewritingVariableName,
  )
 import qualified Kore.Simplify.Ceil as Ceil
+import qualified Kore.Simplify.In as In
 import qualified Kore.Simplify.Not as Not
 import Kore.Simplify.Simplify
 import Kore.Substitute
@@ -68,6 +69,7 @@ import Kore.Syntax (
     Forall (Forall),
     Iff (..),
     Implies (..),
+    In (..),
     Not (..),
     Or (..),
     SomeVariableName,
@@ -178,6 +180,8 @@ simplify sideCondition original =
                 ForallF forallF ->
                     traverse worker (Forall.refreshForall avoid forallF)
                         >>= simplifyForall sideCondition
+                InF inF ->
+                    simplifyIn sideCondition =<< traverse simplifyTerm inF
                 _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT
       where
         _ :< predicateF = Recursive.project predicate
@@ -522,3 +526,11 @@ extractFirstAssignment someVariableName predicates =
         guard (TermLike.isFunctionPattern termLike)
         (guard . not) (someVariableName `occursIn` termLike)
         pure termLike
+
+simplifyIn ::
+    MonadSimplify simplifier =>
+    SideCondition RewritingVariableName ->
+    In sort (OrPattern RewritingVariableName) ->
+    simplifier NormalForm
+simplifyIn sideCondition =
+    In.simplify sideCondition >=> return . MultiOr.map (from @(Condition _))
diff --git a/kore/test/Test/Kore/Simplify/Predicate.hs b/kore/test/Test/Kore/Simplify/Predicate.hs
index d24477e891..b0727e2326 100644
--- a/kore/test/Test/Kore/Simplify/Predicate.hs
+++ b/kore/test/Test/Kore/Simplify/Predicate.hs
@@ -20,6 +20,7 @@ import Kore.Internal.TermLike (
     TermLike,
     mkAnd,
     mkBottom,
+    mkCeil,
     mkElemVar,
     mkEquals,
     mkNot,
@@ -328,6 +329,34 @@ test_simplify =
             (fromEquals_ (mkElemVar x) (mkElemVar y))
             [[fromEquals_ (mkElemVar x) (mkElemVar y)]]
         ]
+    , testGroup
+        "\\in"
+        [ test
+            "\\top"
+            (fromIn_ Mock.a Mock.a)
+            [[]]
+        , test
+            "\\bottom"
+            (fromIn_ Mock.a Mock.b)
+            []
+        , test
+            "\\ceil"
+            (fromIn_ fa fa)
+            [[faCeil]]
+        , test
+            "\\or"
+            (fromIn_ (mkElemVar Mock.xConfig) (mkOr fa fb))
+            [ [faCeil, fromEquals_ (mkElemVar Mock.xConfig) fa]
+            , [fbCeil, fromEquals_ (mkElemVar Mock.xConfig) fb]
+            ]
+        , test
+            "Predicates"
+            ( fromIn_
+                (mkEquals Mock.testSort (mkElemVar Mock.xConfig) fb)
+                (mkCeil Mock.testSort fa)
+            )
+            [[fromEquals_ (mkElemVar Mock.xConfig) fb, faCeil, fbCeil]]
+        ]
     , testGroup
         "Other"
         [ test