diff --git a/plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs b/plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs
index d5df5c77a1a..d424fe5108b 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs
@@ -49,7 +49,7 @@ import PlutusCore.Core.Type (Type (..))
 import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
 import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
 import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing
-import PlutusCore.Data (Data)
+import PlutusCore.Data (Data (..))
 import PlutusCore.Evaluation.Machine.ExMemoryUsage (IntegerCostedLiterally (..),
                                                     NumBytesCostedAsNumWords (..))
 import PlutusCore.Pretty.Extra (juxtRenderContext)
@@ -544,7 +544,18 @@ instance AnnotateCaseBuiltin DefaultUni where
             [cons]      -> Right [(cons, [argTy, listTy])]
             [cons, nil] -> Right [(cons, [argTy, listTy]), (nil, [])]
             _           -> Left $ "Casing on list requires exactly one branch or two branches"
-        _                 -> Left $ display (() <$ ty) <> " isn't supported in 'case'"
+        TyBuiltin ann (SomeTypeIn DefaultUniData) ->
+          case branches of
+            [constr, maep, list, i , b] ->
+              Right
+                [ (constr, [mkTyBuiltin @_ @Integer ann, mkTyBuiltin @_ @[Data] ann])
+                , (maep, [mkTyBuiltin @_ @[(Data, Data)] ann])
+                , (list, [mkTyBuiltin @_ @[Data] ann])
+                , (i, [mkTyBuiltin @_ @Integer ann])
+                , (b, [mkTyBuiltin @_ @ByteString ann])
+                ]
+            _           -> Left $ "Casing on data requires exactly five branches"
+        _               -> Left $ display (() <$ ty) <> " isn't supported in 'case'"
 
 instance CaseBuiltin DefaultUni where
     caseBuiltin someVal@(Some (ValueOf uni x)) branches = case uni of
@@ -568,6 +579,20 @@ instance CaseBuiltin DefaultUni where
                 []       -> Right $ HeadOnly $ branches Vector.! 1
                 (y : ys) -> Right $ headSpine (branches Vector.! 0) [someValueOf ty y, someValueOf uni ys]
             | otherwise            -> Left $ outOfBoundsErr someVal branches
+        DefaultUniData
+            | len == 5 ->
+              case x of
+                Constr idx ds ->
+                  Right $ headSpine (branches Vector.! 0) [someValue @Integer idx, someValue @[Data] ds]
+                Map ds ->
+                  Right $ headSpine (branches Vector.! 1) [someValue @[(Data, Data)] ds]
+                List ds ->
+                  Right $ headSpine (branches Vector.! 2) [someValue @[Data] ds]
+                I i ->
+                  Right $ headSpine (branches Vector.! 3) [someValue @Integer i]
+                B b ->
+                  Right $ headSpine (branches Vector.! 4) [someValue @ByteString b]
+            | otherwise -> Left $ outOfBoundsErr someVal branches
         _ -> Left $ display uni <> " isn't supported in 'case'"
       where
         !len = Vector.length branches
diff --git a/plutus-metatheory/src/MAlonzo/Code/Utils/Decidable.hs b/plutus-metatheory/src/MAlonzo/Code/Utils/Decidable.hs
index da0d1a1a157..fb4c923a58a 100644
--- a/plutus-metatheory/src/MAlonzo/Code/Utils/Decidable.hs
+++ b/plutus-metatheory/src/MAlonzo/Code/Utils/Decidable.hs
@@ -1,29 +1,29 @@
-{-# LANGUAGE BangPatterns              #-}
-{-# LANGUAGE EmptyCase                 #-}
-{-# LANGUAGE EmptyDataDecls            #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE OverloadedStrings         #-}
-{-# LANGUAGE PatternSynonyms           #-}
-{-# LANGUAGE RankNTypes                #-}
-{-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 {-# OPTIONS_GHC -Wno-overlapping-patterns #-}
 
 module MAlonzo.Code.Utils.Decidable where
 
-import Data.Text qualified
-import MAlonzo.Code.Agda.Builtin.Bool qualified
-import MAlonzo.Code.Agda.Builtin.Equality qualified
-import MAlonzo.Code.Agda.Builtin.Sigma qualified
-import MAlonzo.Code.Agda.Primitive qualified
-import MAlonzo.Code.Data.Irrelevant qualified
-import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
-import MAlonzo.Code.Relation.Nullary.Reflects qualified
-import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
-                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
-                    word64ToNat)
-import MAlonzo.RTE qualified
+import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
+                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
+                    rem64, lt64, eq64, word64FromNat, word64ToNat)
+import qualified MAlonzo.RTE
+import qualified Data.Text
+import qualified MAlonzo.Code.Agda.Builtin.Bool
+import qualified MAlonzo.Code.Agda.Builtin.Equality
+import qualified MAlonzo.Code.Agda.Builtin.Sigma
+import qualified MAlonzo.Code.Agda.Primitive
+import qualified MAlonzo.Code.Data.Irrelevant
+import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
+import qualified MAlonzo.Code.Relation.Nullary.Reflects
 
 -- Utils.Decidable.dmap
 d_dmap_12 ::
diff --git a/plutus-metatheory/src/MAlonzo/Code/Utils/Reflection.hs b/plutus-metatheory/src/MAlonzo/Code/Utils/Reflection.hs
index 4f903a4f591..754d48bef63 100644
--- a/plutus-metatheory/src/MAlonzo/Code/Utils/Reflection.hs
+++ b/plutus-metatheory/src/MAlonzo/Code/Utils/Reflection.hs
@@ -1,32 +1,32 @@
-{-# LANGUAGE BangPatterns              #-}
-{-# LANGUAGE EmptyCase                 #-}
-{-# LANGUAGE EmptyDataDecls            #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE OverloadedStrings         #-}
-{-# LANGUAGE PatternSynonyms           #-}
-{-# LANGUAGE RankNTypes                #-}
-{-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 {-# OPTIONS_GHC -Wno-overlapping-patterns #-}
 
 module MAlonzo.Code.Utils.Reflection where
 
-import Data.Text qualified
-import MAlonzo.Code.Agda.Builtin.List qualified
-import MAlonzo.Code.Agda.Builtin.Maybe qualified
-import MAlonzo.Code.Agda.Builtin.Reflection qualified
-import MAlonzo.Code.Agda.Builtin.Sigma qualified
-import MAlonzo.Code.Agda.Builtin.String qualified
-import MAlonzo.Code.Agda.Primitive qualified
-import MAlonzo.Code.Data.Char.Base qualified
-import MAlonzo.Code.Data.List.Base qualified
-import MAlonzo.Code.Data.String.Base qualified
-import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
-import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
-                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
-                    word64ToNat)
-import MAlonzo.RTE qualified
+import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
+                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
+                    rem64, lt64, eq64, word64FromNat, word64ToNat)
+import qualified MAlonzo.RTE
+import qualified Data.Text
+import qualified MAlonzo.Code.Agda.Builtin.List
+import qualified MAlonzo.Code.Agda.Builtin.Maybe
+import qualified MAlonzo.Code.Agda.Builtin.Reflection
+import qualified MAlonzo.Code.Agda.Builtin.Sigma
+import qualified MAlonzo.Code.Agda.Builtin.String
+import qualified MAlonzo.Code.Agda.Primitive
+import qualified MAlonzo.Code.Data.Char.Base
+import qualified MAlonzo.Code.Data.List.Base
+import qualified MAlonzo.Code.Data.String.Base
+import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
 
 -- Utils.Reflection.constructors
 d_constructors_4 ::
@@ -62,7 +62,7 @@ d_lastName_14 v0 v1
       (case coe v2 of
          MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 v3 -> coe v3
          MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> coe v0
-         _                                            -> MAlonzo.RTE.mazUnreachableError)
+         _ -> MAlonzo.RTE.mazUnreachableError)
 -- Utils.Reflection.getLastName
 d_getLastName_34 ::
   AgdaAny -> MAlonzo.Code.Agda.Builtin.String.T_String_6
diff --git a/plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs b/plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs
index 364359e9fea..f66035cd172 100644
--- a/plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs
+++ b/plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs
@@ -451,6 +451,131 @@ defineBuiltinTerms = do
             [PIR.var () f, PIR.var () z]
 
 
+  defineBuiltinTerm annMayInline 'Builtins.caseData' $ case datatypeStyle of
+    style | style == PIR.ScottEncoding || style == PIR.SumsOfProducts ->
+      -- > /\r ->
+      -- >   \(fConstr : integer -> list data -> r)
+      -- >    (fMap : list (pair data data) -> r)
+      -- >    (fList : list data -> r)
+      -- >    (fI : integer -> r)
+      -- >    (fB : bytestring -> r)
+      -- >    (d : data) ->
+      -- >     chooseData
+      -- >       {all dead. r}
+      -- >       d
+      -- >       (/\dead ->
+      -- >          (/\a b c ->
+      -- >             \(f : a -> b -> c) (p : pair a b) ->
+      -- >               f (fstPair {a} {b} p) (sndPair {a} {b} p))
+      -- >            {integer}
+      -- >            {list data}
+      -- >            {r}
+      -- >            fConstr
+      -- >            (unConstrData d))
+      -- >       (/\dead -> fMap (unMapData d))
+      -- >       (/\dead -> fList (unListData d))
+      -- >       (/\dead -> fI (unIData d))
+      -- >       (/\dead -> fB (unBData d))
+      -- >       {r}
+      fmap (const annMayInline) . runQuote $ do
+        r <- freshTyName "r"
+        dead <- freshTyName "dead"
+        fConstr <- freshName "fConstr"
+        fMap <- freshName "fMap"
+        fList <- freshName "fList"
+        fI <- freshName "fI"
+        fB <- freshName "fB"
+        d <- freshName "d"
+        let integer = PLC.mkTyBuiltin @_ @Integer ()
+            listData = PLC.mkTyBuiltin @_ @[PLC.Data] ()
+            listPairData = PLC.mkTyBuiltin @_ @[(PLC.Data, PLC.Data)] ()
+            bytestring = PLC.mkTyBuiltin @_ @BS.ByteString ()
+        return
+          . PIR.tyAbs () r (PLC.Type ())
+          . PIR.lamAbs
+            ()
+            fConstr
+            (PLC.TyFun () integer . PLC.TyFun () listData $ PLC.TyVar () r)
+          . PIR.lamAbs () fMap (PLC.TyFun () listPairData $ PLC.TyVar () r)
+          . PIR.lamAbs () fList (PLC.TyFun () listData $ PLC.TyVar () r)
+          . PIR.lamAbs () fI (PLC.TyFun () integer $ PLC.TyVar () r)
+          . PIR.lamAbs () fB (PLC.TyFun () bytestring $ PLC.TyVar () r)
+          . PIR.lamAbs () d (PLC.mkTyBuiltin @_ @PLC.Data ())
+          . PIR.tyInst
+            ()
+            ( PIR.mkIterAppNoAnn
+                ( PIR.tyInst () (PIR.builtin () PLC.ChooseData)
+                    . PLC.TyForall () dead (PLC.Type ())
+                    $ PLC.TyVar () r
+                )
+                [ PIR.var () d
+                , PIR.tyAbs () dead (PLC.Type ()) $
+                    PIR.mkIterAppNoAnn
+                      ( PIR.mkIterInstNoAnn
+                          PLC.uncurry
+                          [integer, listData, PLC.TyVar () r]
+                      )
+                      [ PIR.var () fConstr
+                      , PIR.apply () (PIR.builtin () PLC.UnConstrData) $
+                          PIR.var () d
+                      ]
+                , PIR.tyAbs () dead (PLC.Type ())
+                    . PIR.apply () (PIR.var () fMap)
+                    . PIR.apply () (PIR.builtin () PLC.UnMapData)
+                    $ PIR.var () d
+                , PIR.tyAbs () dead (PLC.Type ())
+                    . PIR.apply () (PIR.var () fList)
+                    . PIR.apply () (PIR.builtin () PLC.UnListData)
+                    $ PIR.var () d
+                , PIR.tyAbs () dead (PLC.Type ())
+                    . PIR.apply () (PIR.var () fI)
+                    . PIR.apply () (PIR.builtin () PLC.UnIData)
+                    $ PIR.var () d
+                , PIR.tyAbs () dead (PLC.Type ())
+                    . PIR.apply () (PIR.var () fB)
+                    . PIR.apply () (PIR.builtin () PLC.UnBData)
+                    $ PIR.var () d
+                ]
+            )
+          $ PLC.TyVar () r
+    _BuiltinCasing ->
+      -- > /\r ->
+      -- >   \(fConstr : integer -> list data -> r)
+      -- >    (fMap : list (pair data data) -> r)
+      -- >    (fList : list data -> r)
+      -- >    (fI : integer -> r)
+      -- >    (fB : bytestring -> r)
+      -- >    (d : data) ->
+      -- >      (case r d fConstr fMap fList fI fB)
+      fmap (const annMayInline) . runQuote $ do
+        r <- freshTyName "r"
+        fConstr <- freshName "fConstr"
+        fMap <- freshName "fMap"
+        fList <- freshName "fList"
+        fI <- freshName "fI"
+        fB <- freshName "fB"
+        d <- freshName "d"
+        let integer = PLC.mkTyBuiltin @_ @Integer ()
+            listData = PLC.mkTyBuiltin @_ @[PLC.Data] ()
+            listPairData = PLC.mkTyBuiltin @_ @[(PLC.Data, PLC.Data)] ()
+            bytestring = PLC.mkTyBuiltin @_ @BS.ByteString ()
+        return
+          $ PIR.tyAbs () r (PLC.Type ())
+          $ PIR.lamAbs
+            ()
+            fConstr
+            (PLC.TyFun () integer . PLC.TyFun () listData $ PLC.TyVar () r)
+          $ PIR.lamAbs () fMap (PLC.TyFun () listPairData $ PLC.TyVar () r)
+          $ PIR.lamAbs () fList (PLC.TyFun () listData $ PLC.TyVar () r)
+          $ PIR.lamAbs () fI (PLC.TyFun () integer $ PLC.TyVar () r)
+          $ PIR.lamAbs () fB (PLC.TyFun () bytestring $ PLC.TyVar () r)
+          $ PIR.lamAbs () d (PLC.mkTyBuiltin @_ @PLC.Data ())
+          $ PIR.kase
+            ()
+            (PLC.TyVar () r)
+            (PIR.var () d)
+            [PIR.var () fConstr, PIR.var () fMap, PIR.var () fList, PIR.var () fI, PIR.var () fB]
+
   -- See Note [Builtin terms and values]
   for_ enumerate $ \fun ->
     let defineBuiltinInl impl = defineBuiltinTerm annMayInline impl $ mkBuiltin fun