diff --git a/kore/src/Kore/Reachability/Claim.hs b/kore/src/Kore/Reachability/Claim.hs
index e4f045ef3e..48b74ebba5 100644
--- a/kore/src/Kore/Reachability/Claim.hs
+++ b/kore/src/Kore/Reachability/Claim.hs
@@ -590,9 +590,16 @@ simplify' ::
     Strategy.TransitionT (AppliedRule claim) m claim
 simplify' lensClaimPattern claim = do
     claim' <- simplifyLeftHandSide claim
-    let sideCondition = extractSideCondition claim'
-    simplifyRightHandSide lensClaimPattern sideCondition claim'
+    let claim'' = Lens.over lensClaimPattern applySubstOnRightHandSide claim'
+        sideCondition = extractSideCondition claim''
+    simplifyRightHandSide lensClaimPattern sideCondition claim''
   where
+    applySubstOnRightHandSide claimPat =
+        let substitution = Pattern.substitution $ Lens.view (field @"left") claimPat
+            noLeftSubst = Lens.set (field @"left" . field @"substitution") mempty claimPat
+            appliedSubst = ClaimPattern.applySubstitution substitution noLeftSubst
+         in appliedSubst
+
     extractSideCondition =
         SideCondition.fromConditionWithReplacements
             . Pattern.withoutTerm
diff --git a/kore/test/Test/Kore/Reachability/OnePathStrategy.hs b/kore/test/Test/Kore/Reachability/OnePathStrategy.hs
index 38715883a2..b629938ee0 100644
--- a/kore/test/Test/Kore/Reachability/OnePathStrategy.hs
+++ b/kore/test/Test/Kore/Reachability/OnePathStrategy.hs
@@ -808,9 +808,7 @@ test_onePathStrategy =
                         )
                     )
             left' =
-                Pattern.withCondition
-                    Mock.a
-                    (Condition.assign (inject Mock.x) Mock.a)
+                Pattern.fromTermLike Mock.a
             right =
                 Pattern.withCondition
                     (TermLike.mkElemVar Mock.x)
diff --git a/kore/test/Test/Kore/Reachability/Prove.hs b/kore/test/Test/Kore/Reachability/Prove.hs
index f645e7d394..0c2b3eea76 100644
--- a/kore/test/Test/Kore/Reachability/Prove.hs
+++ b/kore/test/Test/Kore/Reachability/Prove.hs
@@ -426,9 +426,7 @@ test_proveClaims =
                                 )
                             )
                         )
-                    , Pattern.withCondition
-                        Mock.b
-                        (Condition.assign (inject Mock.x) Mock.a)
+                    , Pattern.fromTermLike Mock.b
                     ]
             initialPattern =
                 Pattern.fromTermLike
diff --git a/test/issue-2221/test-issue-2221.sh.out.golden b/test/issue-2221/test-issue-2221.sh.out.golden
index f438df9b12..04dba5204f 100644
--- a/test/issue-2221/test-issue-2221.sh.out.golden
+++ b/test/issue-2221/test-issue-2221.sh.out.golden
@@ -1,33 +1,10 @@
-/* Created: Kore.Internal.OrPattern.toTermLike */
-/* Spa */
-\and{SortGeneratedTopCell{}}(
+/* Fl Fn D Sfa */
+Lbl'-LT-'generatedTop'-GT-'{}(
+    /* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()),
     /* Fl Fn D Sfa */
-    Lbl'-LT-'generatedTop'-GT-'{}(
-        /* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()),
-        /* Fl Fn D Sfa */
-        Lbl'-LT-'generatedCounter'-GT-'{}(
-            /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{}
-        ),
-        /* Fl Fn D Sfa Cl */
-        Lbl'-LT-'size'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1"))
+    Lbl'-LT-'generatedCounter'-GT-'{}(
+        /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{}
     ),
-    /* Spa */
-    \and{SortGeneratedTopCell{}}(
-        /* Spa */
-        \equals{SortMyList{}, SortGeneratedTopCell{}}(
-            /* Fl Fn D Sfa */ Var'Unds'0:SortMyList{},
-            /* Fl Fn D Sfa */
-            Lbl'UndsUndsUnds'LIST-SIZER-SYNTAX'Unds'MyList'Unds'Int'Unds'MyList{}(
-                /* Fl Fn D Sfa */ Var'Unds'E:SortInt{},
-                /* Fl Fn D Sfa Cl */
-                Lbl'Stop'MyList'Unds'LIST-SIZER-SYNTAX'Unds'MyList{}()
-            )
-        ),
-        /* Spa */
-        \equals{SortMyList{}, SortGeneratedTopCell{}}(
-            /* Fl Fn D Sfa */ VarL:SortMyList{},
-            /* Fl Fn D Sfa Cl */
-            Lbl'Stop'MyList'Unds'LIST-SIZER-SYNTAX'Unds'MyList{}()
-        )
-    )
+    /* Fl Fn D Sfa Cl */
+    Lbl'-LT-'size'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1"))
 )
\ No newline at end of file
diff --git a/test/issue-2244/test-issue-2244.sh.out.golden b/test/issue-2244/test-issue-2244.sh.out.golden
index e3bd16b3c9..11476beae5 100644
--- a/test/issue-2244/test-issue-2244.sh.out.golden
+++ b/test/issue-2244/test-issue-2244.sh.out.golden
@@ -1,202 +1,178 @@
 /* Created: Kore.Internal.OrPattern.toTermLike */
 /* Spa */
 \and{SortGeneratedTopCell{}}(
-    /* Created: Kore.Internal.OrPattern.toTermLike */
-    /* Spa */
-    \and{SortGeneratedTopCell{}}(
+    /* Fl Fn D Sfa */
+    Lbl'-LT-'generatedTop'-GT-'{}(
         /* Fl Fn D Sfa */
-        Lbl'-LT-'generatedTop'-GT-'{}(
+        Lbl'-LT-'michelsonTop'-GT-'{}(
             /* Fl Fn D Sfa */
-            Lbl'-LT-'michelsonTop'-GT-'{}(
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'paramtype'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'24:SortPreType{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'paramvalue'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'25:SortPreData{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'storagetype'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'26:SortPreType{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'storagevalue'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'27:SortPreData{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'mybalance'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'28:SortMutez{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'myamount'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'29:SortMutez{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'mynow'-GT-'{}(
-                    /* Fl Fn D Sfa */
-                    Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}(
-                        /* Fl Fn D Sfa */ Var'Unds'30:SortInt{}
-                    )
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'myaddr'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'31:SortAddress{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'knownaddrs'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'32:SortMap{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'sourceaddr'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'33:SortAddress{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'senderaddr'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'34:SortAddress{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'mychainid'-GT-'{}(
-                    /* Fl Fn D Sfa */
-                    Lbl'Hash'ChainId'LParUndsRParUnds'MICHELSON-COMMON'Unds'ChainId'Unds'MichelsonBytes{}(
-                        /* Fl Fn D Sfa */ Var'Unds'35:SortMichelsonBytes{}
-                    )
-                ),
+            Lbl'-LT-'paramtype'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'24:SortPreType{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'paramvalue'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'25:SortPreData{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'storagetype'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'26:SortPreType{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'storagevalue'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'27:SortPreData{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'mybalance'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'28:SortMutez{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'myamount'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'29:SortMutez{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'mynow'-GT-'{}(
                 /* Fl Fn D Sfa */
-                Lbl'-LT-'nonce'-GT-'{}(
-                    /* Fl Fn D Sfa */
-                    Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}(
-                        /* Fl Fn D Sfa */ Var'Unds'36:SortInt{}
-                    )
-                ),
+                Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}(
+                    /* Fl Fn D Sfa */ Var'Unds'30:SortInt{}
+                )
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'myaddr'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'31:SortAddress{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'knownaddrs'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'32:SortMap{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'sourceaddr'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'33:SortAddress{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'senderaddr'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'34:SortAddress{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'mychainid'-GT-'{}(
                 /* Fl Fn D Sfa */
-                Lbl'-LT-'bigmaps'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'37:SortMap{}
-                ),
+                Lbl'Hash'ChainId'LParUndsRParUnds'MICHELSON-COMMON'Unds'ChainId'Unds'MichelsonBytes{}(
+                    /* Fl Fn D Sfa */ Var'Unds'35:SortMichelsonBytes{}
+                )
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'nonce'-GT-'{}(
                 /* Fl Fn D Sfa */
-                Lbl'-LT-'script'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'38:SortPreData{}
-                ),
-                /* Fl Fn D Sfa Cl */
-                Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()),
+                Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}(
+                    /* Fl Fn D Sfa */ Var'Unds'36:SortInt{}
+                )
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'bigmaps'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'37:SortMap{}),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'script'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'38:SortPreData{}
+            ),
+            /* Fl Fn D Sfa Cl */
+            Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'stack'-GT-'{}(
                 /* Fl Fn D Sfa */
-                Lbl'-LT-'stack'-GT-'{}(
+                /* Inj: */ inj{SortStack{}, SortInternalStack{}}(
                     /* Fl Fn D Sfa */
-                    /* Inj: */ inj{SortStack{}, SortInternalStack{}}(
+                    Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}(
                         /* Fl Fn D Sfa */
-                        Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}(
+                        Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}(
+                            /* Fl Fn D Sfa Cli */
+                            /* Inj: */ inj{SortNumTypeName{}, SortTypeName{}}(
+                                /* Fl Fn D Sfa Cl */
+                                Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}()
+                            ),
                             /* Fl Fn D Sfa */
-                            Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}(
-                                /* Fl Fn D Sfa Cli */
-                                /* Inj: */ inj{SortNumTypeName{}, SortTypeName{}}(
-                                    /* Fl Fn D Sfa Cl */
-                                    Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}()
-                                ),
+                            /* Inj: */ inj{SortInt{}, SortData{}}(
                                 /* Fl Fn D Sfa */
-                                /* Inj: */ inj{SortInt{}, SortData{}}(
+                                Lbl'UndsPlus'Int'Unds'{}(
                                     /* Fl Fn D Sfa */
-                                    Lbl'UndsPlus'Int'Unds'{}(
-                                        /* Fl Fn D Sfa */
-                                        Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
-                                            /* Fl Fn D Sfa */
-                                            VarL:SortInternalList{},
-                                            /* Fl Fn D Sfa Cl */
-                                            \dv{SortInt{}}("0")
-                                        ),
+                                    Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
                                         /* Fl Fn D Sfa */
-                                        Lbl'UndsPlus'Int'Unds'{}(
-                                            /* Fl Fn D Sfa */ VarI:SortInt{},
-                                            /* Fl Fn D Sfa Cl */
-                                            \dv{SortInt{}}("1")
-                                        )
+                                        VarL:SortInternalList{},
+                                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
+                                    ),
+                                    /* Fl Fn D Sfa */
+                                    Lbl'UndsPlus'Int'Unds'{}(
+                                        /* Fl Fn D Sfa */ VarI:SortInt{},
+                                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
                                     )
                                 )
-                            ),
-                            /* Fl Fn D Sfa Cl */
-                            Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack'QuotRBraUnds'Stack{}()
-                        )
-                    )
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'inputstack'-GT-'{}(
-                    /* Fl Fn D Sfa */
-                    Lbl'LBraUndsRBraUnds'UNIT-TEST-COMMON-SYNTAX'Unds'LiteralStack'Unds'StackElementList{}(
-                        /* Fl Fn D Sfa */ Var'Unds'39:SortStackElementList{}
+                            )
+                        ),
+                        /* Fl Fn D Sfa Cl */
+                        Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack'QuotRBraUnds'Stack{}()
                     )
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'expected'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'40:SortOutputStack{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'pre'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'41:SortBlockList{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'post'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'42:SortBlockList{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'invs'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'43:SortMap{}),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'symbols'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'44:SortMap{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'returncode'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'45:SortInt{}
-                ),
-                /* Fl Fn D Sfa */
-                Lbl'-LT-'assumeFailed'-GT-'{}(
-                    /* Fl Fn D Sfa */ Var'Unds'46:SortBool{}
-                ),
+                )
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'inputstack'-GT-'{}(
                 /* Fl Fn D Sfa */
-                Lbl'-LT-'trace'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'47:SortK{})
+                Lbl'LBraUndsRBraUnds'UNIT-TEST-COMMON-SYNTAX'Unds'LiteralStack'Unds'StackElementList{}(
+                    /* Fl Fn D Sfa */ Var'Unds'39:SortStackElementList{}
+                )
             ),
             /* Fl Fn D Sfa */
-            Lbl'-LT-'generatedCounter'-GT-'{}(
-                /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{}
-            )
+            Lbl'-LT-'expected'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'40:SortOutputStack{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'pre'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'41:SortBlockList{}),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'post'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'42:SortBlockList{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'invs'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'43:SortMap{}),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'symbols'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'44:SortMap{}),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'returncode'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'45:SortInt{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'assumeFailed'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'46:SortBool{}
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'trace'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'47:SortK{})
         ),
+        /* Fl Fn D Sfa */
+        Lbl'-LT-'generatedCounter'-GT-'{}(
+            /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{}
+        )
+    ),
+    /* Sfa */
+    \not{SortGeneratedTopCell{}}(
         /* Sfa */
-        \not{SortGeneratedTopCell{}}(
-            /* Sfa */
-            \equals{SortInt{}, SortGeneratedTopCell{}}(
+        \equals{SortInt{}, SortGeneratedTopCell{}}(
+            /* Fl Fn D Sfa */
+            Lbl'UndsPlus'Int'Unds'{}(
                 /* Fl Fn D Sfa */
-                Lbl'UndsPlus'Int'Unds'{}(
-                    /* Fl Fn D Sfa */
-                    Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
-                        /* Fl Fn D Sfa */ VarL:SortInternalList{},
-                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
-                    ),
-                    /* Fl Fn D Sfa */
-                    Lbl'UndsPlus'Int'Unds'{}(
-                        /* Fl Fn D Sfa */ VarI:SortInt{},
-                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
-                    )
+                Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
+                    /* Fl Fn D Sfa */ VarL:SortInternalList{},
+                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
                 ),
                 /* Fl Fn D Sfa */
                 Lbl'UndsPlus'Int'Unds'{}(
-                    /* Fl Fn D Sfa */
-                    Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
-                        /* Fl Fn D Sfa */ VarL:SortInternalList{},
-                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
-                    ),
-                    /* Fl Fn D Sfa */ VarI:SortInt{}
+                    /* Fl Fn D Sfa */ VarI:SortInt{},
+                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
                 )
-            )
-        )
-    ),
-    /* Spa */
-    \equals{SortInternalList{}, SortGeneratedTopCell{}}(
-        /* Fl Fn D Sfa */ VarIntList:SortInternalList{},
-        /* Fl Fn D Sfa */
-        Lbl'UndsSClnSClnUndsUnds'MICHELSON-COMMON'Unds'InternalList'Unds'WrappedData'Unds'InternalList{}(
-            /* Fl Fn D Sfa */
-            Lbl'LSqBUndsRSqBUnds'MICHELSON-COMMON'Unds'WrappedData'Unds'Data{}(
-                /* Fl Fn D Sfa */ VarE:SortData{}
             ),
-            /* Fl Fn D Sfa */ VarL:SortInternalList{}
+            /* Fl Fn D Sfa */
+            Lbl'UndsPlus'Int'Unds'{}(
+                /* Fl Fn D Sfa */
+                Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
+                    /* Fl Fn D Sfa */ VarL:SortInternalList{},
+                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
+                ),
+                /* Fl Fn D Sfa */ VarI:SortInt{}
+            )
         )
     )
 )
\ No newline at end of file
diff --git a/test/issue-2740/Makefile b/test/issue-2740/Makefile
new file mode 100644
index 0000000000..a72c5f37d2
--- /dev/null
+++ b/test/issue-2740/Makefile
@@ -0,0 +1,2 @@
+DEF = either
+include $(CURDIR)/../include.mk
\ No newline at end of file
diff --git a/test/issue-2740/either-spec.k b/test/issue-2740/either-spec.k
new file mode 100644
index 0000000000..95780a818c
--- /dev/null
+++ b/test/issue-2740/either-spec.k
@@ -0,0 +1,15 @@
+module VERIFICATION
+  imports EITHER
+
+  syntax KItem ::= run ( Either, Int ) | done ( Either )
+  rule run(Left(),  _I) => done(Left())
+  rule run(Right(), _I) => done(Right())
+endmodule
+
+module EITHER-SPEC
+  imports VERIFICATION
+
+  claim <k> run(E,I) => done(E) ... </k>
+    requires I >Int 0
+    ensures P(E,I)
+endmodule
diff --git a/test/issue-2740/either-spec.k.out.golden b/test/issue-2740/either-spec.k.out.golden
new file mode 100644
index 0000000000..17a1d4510e
--- /dev/null
+++ b/test/issue-2740/either-spec.k.out.golden
@@ -0,0 +1 @@
+#Top
diff --git a/test/issue-2740/either.k b/test/issue-2740/either.k
new file mode 100644
index 0000000000..5c4682eb01
--- /dev/null
+++ b/test/issue-2740/either.k
@@ -0,0 +1,14 @@
+module EITHER
+  imports INT
+
+  syntax Either ::= Left() | Right()
+  syntax Bool ::= P( Either , Int ) [function]
+
+  rule P(Left(),I) => true
+    requires I >Int 0
+  rule P(Right(),I) => true
+    requires I >Int 0
+  rule P(_E,I) => false
+    requires I <=Int 0
+
+endmodule