diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -8,3 +8,10 @@
 
 * Redesign from scratch.
 * Released as a beta version.
+
+## 0.3.0.0 -- 2024-09-01
+
+* Fixed #7: bug on `interposeRecH`. https://github.com/sayo-hs/heftia/issues/7
+* Fixed #8: bug on `subsume`. https://github.com/sayo-hs/heftia/issues/8
+* Added effect list manipulation functions such as `raiseNUnderM`. https://github.com/sayo-hs/heftia/issues/4
+* Update the data-effects version to 0.1.1.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -27,8 +27,57 @@
 
 **We are looking forward to your feedback!**
 
+## Installation
+1.
+    ```console
+    $ cabal update
+    ```
+2. Add `heftia-effects ^>= 0.2` and `ghc-typelits-knownnat ^>= 0.7` to the build dependencies. Enable the [ghc-typelits-knownnat](https://hackage.haskell.org/package/ghc-typelits-knownnat) plugin, `GHC2021`, and the following language extensions as needed:
+
+    * `LambdaCase`
+    * `DerivingStrategies`
+    * `DataKinds`
+    * `TypeFamilies`
+    * `BlockArguments`
+    * `FunctionalDependencies`
+    * `RecordWildCards`
+    * `DefaultSignatures`
+    * `PatternSynonyms`
+
+Example .cabal:
+
+```
+...
+    build-depends:
+        ...
+        heftia-effects ^>= 0.2,
+        ghc-typelits-knownnat ^>= 0.7,
+
+    default-language: GHC2021
+
+    default-extensions:
+        ...
+        LambdaCase,
+        DerivingStrategies,
+        DataKinds,
+        TypeFamilies,
+        BlockArguments,
+        FunctionalDependencies,
+        RecordWildCards,
+        DefaultSignatures,
+        PatternSynonyms,
+        TemplateHaskell,
+        PartialTypeSignatures,
+        AllowAmbiguousTypes
+
+    ghc-options: ... -fplugin GHC.TypeLits.KnownNat.Solver
+...
+```
+
+This library has been tested to work with GHC 9.2.8.
+
 ## Getting Started
-To run the [SemanticsZoo example](heftia-effects/Example/SemanticsZoo/Main.hs):
+To run the [SemanticsZoo example](https://github.com/sayo-hs/heftia/blob/v0.3.0/heftia-effects/Example/SemanticsZoo/Main.hs):
 ```console
 $ git clone https://github.com/sayo-hs/heftia
 $ cd heftia/heftia-effects
@@ -63,7 +112,7 @@
 In handling higher-order effects, it's easy to work with **multi-shot delimited continuations**.
 This enables an almost complete emulation of "Algebraic Effects and Handlers".
 For more details, please refer to
-the [example code](heftia-effects/Example/Continuation/Main.hs).
+the [example code](https://github.com/sayo-hs/heftia/blob/v0.3.0/heftia-effects/Example/Continuation/Main.hs).
 
 ### Two interpretations of the `censor` effect for Writer
 
@@ -116,7 +165,7 @@
 Post-applying: Hello world!!
 ```
 
-For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/develop/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/develop/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs).
+For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/v0.3.0/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/v0.3.0/heftia-effects/src/Control/Effect/Interpreter/Heftia/Writer.hs).
 
 Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being
 eliminated.
@@ -127,47 +176,34 @@
 Heftia is the current main focus of the [Sayo Project](https://github.com/sayo-hs).
 
 ## Documentation
-The example codes are located in the [heftia-effects/Example/](heftia-effects/Example/) directory.
+The example codes are located in the [heftia-effects/Example/](https://github.com/sayo-hs/heftia/tree/v0.3.0/heftia-effects/Example) directory.
 Also, the following *HeftWorld* example: https://github.com/sayo-hs/HeftWorld
 
-~~Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory.~~ Documents have become outdated.
-Please wait for the documentation for the new version to be written.
-
-## Limitation and how to avoid it
-### The *reset* behavior of the scopes held by unhandled higher-order effects
-When attempting to interpret an effect while there are unhandled higher-order effects present, you cannot obtain delimited continuations beyond the action scope held by these unhandled higher-order effects.
-It appears as if a *reset* (in the sense of *shift/reset*) is applied to each of the scopes still held by the remaining unhandled higher-order effects.
-
-In other words, to obtain delimited continuations beyond their scope, it is necessary to first handle and eliminate all higher-order effects that hold those scopes,
-and then handle the effect targeted for stateful interpretation in that order.
-For this purpose, it might sometimes be possible to use *multi-layering*. For an example of multi-layering,
-see `handleReaderThenShift` defined in [Example/Continuation2](https://github.com/sayo-hs/heftia/blob/8f71a2d4e6125018b64cbbacd32151565a29046d/heftia-effects/Example/Continuation2/Main.hs)
-(particularly, the type signature of `prog` within it).
-For more details, please refer to the documentation of the `interpretRec` family of functions.
+Examples with explanations in Japanese can be found in the [docs-ja/examples/](https://github.com/sayo-hs/heftia/tree/v0.3.0/docs-ja/examples) directory.
 
 ## Comparison
 
 * Higher-Order Effects: Does it support higher-order effects?
 * Delimited Continuation: The ability to manipulate delimited continuations.
-* Statically Typed Set of Effects: For a term representing an effectful program, is it possible to statically decidable a type that enumerates all the effects the program may produce?
+* Effect System: For a term representing an effectful program, is it possible to statically decidable a type that enumerates all the effects the program may produce?
 * Purely Monadic: Is an effectful program represented as a transparent data structure that is a monad, and can it be interpreted into other data types using only pure operations without side effects or `unsafePerformIO`?
 * Dynamic Effect Rewriting: Can an effectful program have its internal effects altered afterwards (by functions typically referred to as `handle with`, `intercept`, `interpose`, `transform`, `translate`, or `rewrite`) ?
 * Performance: Time complexity or space complexity.
 
-| Library or Language | Higher-Order Effects | Delimited Continuation | Statically Typed Set of Effects                 | Purely Monadic                    | Dynamic Effect Rewriting | Performance (TODO) |
-| ------------------- | -------------------- | ---------------------- | ----------------------------------------------- | --------------------------------- | ------------------------ | ------------------ |
-| Heftia              | Yes [^1]             | Multi-shot             | Yes                                             | Yes (also Applicative and others) | Yes                      | ?                  |
-| freer-simple        | No                   | Multi-shot             | Yes                                             | Yes                               | Yes                      | ?                  |
-| Polysemy            | Yes                  | No                     | Yes                                             | Yes                               | Yes                      | ?                  |
-| Effectful           | Yes                  | No                     | Yes                                             | No (based on the `IO` monad)      | Yes                      | ?                  |
-| eff                 | Yes                  | Multi-shot?            | Yes                                             | No (based on the `IO` monad)      | Yes                      | Fast               |
-| mtl                 | Yes                  | Multi-shot (`ContT`)   | Yes                                             | Yes                               | No                       | ?                  |
-| fused-effects       | Yes                  | No?                    | Yes                                             | Yes                               | No                       | ?                  |
-| koka-lang           | No?                  | Multi-shot             | Yes                                             | No (language built-in)            | ?                        | ?                  |
-| OCaml-lang 5        | Yes                  | One-shot               | No [^2]                                         | No (language built-in)            | ?                        | ?                  |
+| Library or Language | Higher-Order Effects | Delimited Continuation | Effect System | Purely Monadic                    | Dynamic Effect Rewriting | Performance (TODO) |
+| ------------------- | -------------------- | ---------------------- | --------------| --------------------------------- | ------------------------ | ------------------ |
+| Heftia              | Yes                  | Multi-shot             | Yes           | Yes (also Applicative and others) | Yes                      | ?                  |
+| freer-simple        | No                   | Multi-shot             | Yes           | Yes                               | Yes                      | ?                  |
+| Polysemy            | Yes                  | No                     | Yes           | Yes                               | Yes                      | ?                  |
+| Effectful           | Yes                  | No                     | Yes           | No (based on the `IO` monad)      | Yes                      | ?                  |
+| eff                 | Yes                  | Multi-shot?            | Yes           | No (based on the `IO` monad)      | Yes                      | Fast               |
+| mtl                 | Yes                  | Multi-shot (`ContT`)   | Yes           | Yes                               | No                       | ?                  |
+| fused-effects       | Yes                  | No?                    | Yes           | Yes                               | No                       | ?                  |
+| koka-lang           | No [^2]              | Multi-shot             | Yes           | No (language built-in)            | Yes                      | ?                  |
+| OCaml-lang 5        | ?                    | One-shot               | No [^3]       | No (language built-in)            | ?                        | ?                  |
 
-[^1]: limitation: https://github.com/sayo-hs/heftia?tab=readme-ov-file#the-reset-behavior-of-the-scopes-held-by-unhandled-higher-order-effects
-[^2]: potential for 'unhandled' runtime errors
+[^2]: https://gist.github.com/ymdryo/6fb2f7f4020c6fcda98ccc67c090dc75
+[^3]: Effects do not appear in the type signature and can potentially cause unhandled errors at runtime
 
 Heftia can simply be described as a higher-order version of freer-simple.
 This is indeed true in terms of its internal mechanisms as well.
@@ -185,7 +221,7 @@
 
 * GADTs for higher-order effects need to be instances of the [HFunctor](https://hackage.haskell.org/package/compdata-0.13.1/docs/Data-Comp-Multi-HFunctor.html#t:HFunctor) type class for convenient usage.
     While it is still possible to use them without being instances of `HFunctor`,
-    the `interpretRec` family of functions cannot be used when higher-order effects that are not `HFunctor` are unhandled.
+    the `interpretRec` family of functions cannot be used when higher-order effects that are not `HFunctor` are unelaborated.
     If this issue is not a concern, the GADT representation of higher-order effects is compatible with Polysemy and fused-effects.
     It is not compatible with Effectful and eff.
 
@@ -198,20 +234,19 @@
 ## Future Plans
 * Enriching the documentation and tests
 * Completing missing definitions such as
-    * `raise`, `raiseUnder`, and `subsume` for arbitrary numbers of effects by type classes.
     * more patterns of interpret & transform function-families.
-    * handlers for the `Accum` and others effect classes
+    * interpreters for the `Accum` and others effect classes
 
     and others.
 * Benchmarking
 
 ## License
-The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/develop/NOTICE).
-Additionally, this README.md and the documents under the `docs`/`docs-ja` directory are licensed
+The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/v0.3.0/NOTICE).
+Additionally, this README.md and the documents under the `docs-ja` directory are licensed
 under CC BY-SA 4.0.
 
 ## Your contributions are welcome!
-Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/develop/CONTRIBUTING.md).
+Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/v0.3.0/CONTRIBUTING.md).
 
 ## Credits
 Parts of this project have been inspired by the following resources:
diff --git a/heftia.cabal b/heftia.cabal
--- a/heftia.cabal
+++ b/heftia.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               heftia
-version:            0.2.0.0
+version:            0.3.0.0
 
 -- A short (one-line) description of the package.
 synopsis: higher-order effects done right
@@ -73,6 +73,8 @@
         Control.Monad.Freer.Church
         Control.Monad.Freer.Tree
         Data.Hefty.Union
+        Data.Hefty.Union.Weaken
+        Data.Hefty.Union.Strengthen
         Data.Hefty.Extensible
         Data.Free.Sum
 
@@ -96,7 +98,7 @@
     -- other-extensions:
     build-depends:
         base                          ^>= 4.16.4.0,
-        data-effects                ^>= 0.1,
+        data-effects                ^>= 0.1.1,
         mtl ^>= 2.2.2,
         free ^>= 5.2,
         kan-extensions ^>= 5.2.5,
diff --git a/src/Control/Effect/Free.hs b/src/Control/Effect/Free.hs
--- a/src/Control/Effect/Free.hs
+++ b/src/Control/Effect/Free.hs
@@ -12,7 +12,7 @@
 Portability :  portable
 
 A Freer carrier that can be used as a handler for effect systems based
-on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).
+on [@data-effects@](https://hackage.haskell.org/package/data-effects).
 -}
 module Control.Effect.Free where
 
diff --git a/src/Control/Effect/Hefty.hs b/src/Control/Effect/Hefty.hs
--- a/src/Control/Effect/Hefty.hs
+++ b/src/Control/Effect/Hefty.hs
@@ -12,11 +12,12 @@
 Stability   :  experimental
 Portability :  portable
 
-A Heftia carrier that can be used as a handler for effect systems based
-on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).
+A Hefty carrier that can be used as a handler for effect systems based
+on [@data-effects@](https://hackage.haskell.org/package/data-effects).
 -}
 module Control.Effect.Hefty where
 
+import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
 import Control.Effect.Key (sendInsBy, sendSigBy)
 import Control.Freer (Freer, InjectIns, InjectInsBy, injectIns, injectInsBy, interpretFreer, liftIns, transformFreer)
@@ -27,13 +28,14 @@
 import Control.Monad.Trans (MonadTrans)
 import Data.Coerce (coerce)
 import Data.Effect (LiftIns (LiftIns), Nop, SigClass, unliftIns)
-import Data.Effect.HFunctor (HFunctor, caseH, hfmap, (:+:))
+import Data.Effect.HFunctor (HFunctor, caseH, hfmap, (:+:) (Inl, Inr))
 import Data.Effect.Key (Key (Key), KeyH (KeyH), unKey, unKeyH, type (##>), type (#>))
-import Data.Effect.Tag (Tag (unTag), TagH (unTagH), type (#), type (##))
+import Data.Effect.Tag (Tag (Tag, unTag), TagH (TagH, unTagH), type (#), type (##))
 import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))
 import Data.Hefty.Union (
     HFunctorUnion,
     HFunctorUnion_ (ForallHFunctor),
+    HasMembershipRec,
     HeadIns,
     LiftInsIfSingle (liftInsIfSingle, unliftInsIfSingle),
     Lookup,
@@ -49,17 +51,20 @@
     flipUnion,
     flipUnion3,
     flipUnionUnder,
-    inject,
     injectRec,
     projectRec,
     weaken2,
     weaken2Under,
     weaken2Under2,
+    weaken3,
     weaken3Under,
+    weaken4,
     weakenUnder2,
     weakenUnder3,
     (|+),
  )
+import Data.Hefty.Union.Strengthen (Strengthen, StrengthenUnder, strengthenN, strengthenNUnderM)
+import Data.Hefty.Union.Weaken (Weaken, WeakenUnder, weakenN, weakenNUnderM)
 import Data.Kind (Type)
 import Data.Maybe.Singletons (FromJust)
 
@@ -421,7 +426,7 @@
     e (Eff u fr ehs efs) ~> Eff u fr ehs efs ->
     Eff u fr ehs efs ~> Eff u fr ehs efs
 interposeRecH f =
-    interpretAllH
+    interpretAllRecH
         \u -> case projectRec u of
             Just e -> f e
             Nothing -> injectH u
@@ -808,6 +813,54 @@
                     (L1 . fh . hfmap (transformAllFH fh ff))
                     (R1 . ff)
 
+raiseN ::
+    forall n ef' eh fr u c ef.
+    (Weaken n ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
+    Eff u fr eh ef ~> Eff u fr eh ef'
+raiseN = transformAll $ weakenN @n
+
+raiseNH ::
+    forall n eh' ef fr u c eh.
+    (Weaken n eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
+    Eff u fr eh ef ~> Eff u fr eh' ef
+raiseNH = transformAllH $ weakenN @n
+
+raiseNUnderM ::
+    forall n m ef' eh fr u c ef.
+    (WeakenUnder n m ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
+    Eff u fr eh ef ~> Eff u fr eh ef'
+raiseNUnderM = transformAll $ weakenNUnderM @n @m
+
+raiseNUnderMH ::
+    forall n m eh' ef fr u c eh.
+    (WeakenUnder n m eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
+    Eff u fr eh ef ~> Eff u fr eh' ef
+raiseNUnderMH = transformAllH $ weakenNUnderM @n @m
+
+subsumeN ::
+    forall n ef' eh fr u c ef.
+    (Strengthen n u ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
+    Eff u fr eh ef ~> Eff u fr eh ef'
+subsumeN = transformAll $ strengthenN @n
+
+subsumeNH ::
+    forall n eh' ef fr u c eh.
+    (Strengthen n u eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
+    Eff u fr eh ef ~> Eff u fr eh' ef
+subsumeNH = transformAllH $ strengthenN @n
+
+subsumeNUnderM ::
+    forall n m ef' eh fr u c ef.
+    (StrengthenUnder n m u ef ef', Freer c fr, Union u, HFunctor (u eh)) =>
+    Eff u fr eh ef ~> Eff u fr eh ef'
+subsumeNUnderM = transformAll $ strengthenNUnderM @n @m
+
+subsumeNUnderMH ::
+    forall n m eh' ef fr u c eh.
+    (StrengthenUnder n m u eh eh', Freer c fr, Union u, HFunctor (u eh)) =>
+    Eff u fr eh ef ~> Eff u fr eh' ef
+subsumeNUnderMH = transformAllH $ strengthenNUnderM @n @m
+
 raise ::
     forall e r ehs fr u c.
     (Freer c fr, Union u, HFunctor (u ehs)) =>
@@ -815,6 +868,27 @@
 raise = transformAll weaken
 {-# INLINE raise #-}
 
+raise2 ::
+    forall e2 e1 r ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs)) =>
+    Eff u fr ehs r ~> Eff u fr ehs (e2 ': e1 ': r)
+raise2 = transformAll weaken2
+{-# INLINE raise2 #-}
+
+raise3 ::
+    forall e3 e2 e1 r ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs)) =>
+    Eff u fr ehs r ~> Eff u fr ehs (e3 ': e2 ': e1 ': r)
+raise3 = transformAll weaken3
+{-# INLINE raise3 #-}
+
+raise4 ::
+    forall e4 e3 e2 e1 r ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs)) =>
+    Eff u fr ehs r ~> Eff u fr ehs (e4 ': e3 ': e2 ': e1 ': r)
+raise4 = transformAll weaken4
+{-# INLINE raise4 #-}
+
 raiseH ::
     forall e r efs fr u c.
     (Freer c fr, Union u, HFunctor (u r)) =>
@@ -829,6 +903,20 @@
 raise2H = transformAllH weaken2
 {-# INLINE raise2H #-}
 
+raise3H ::
+    forall e3 e2 e1 r efs fr u c.
+    (Freer c fr, Union u, HFunctor (u r)) =>
+    Eff u fr r efs ~> Eff u fr (e3 ': e2 ': e1 ': r) efs
+raise3H = transformAllH weaken3
+{-# INLINE raise3H #-}
+
+raise4H ::
+    forall e4 e3 e2 e1 r efs fr u c.
+    (Freer c fr, Union u, HFunctor (u r)) =>
+    Eff u fr r efs ~> Eff u fr (e4 ': e3 ': e2 ': e1 ': r) efs
+raise4H = transformAllH weaken4
+{-# INLINE raise4H #-}
+
 raiseUnder ::
     forall e1 e2 r ehs fr u c.
     (Freer c fr, Union u, HFunctor (u ehs)) =>
@@ -971,18 +1059,100 @@
 
 subsume ::
     forall e r ehs fr u c.
-    (Freer c fr, Union u, HFunctor (u ehs), HasMembership u e r) =>
+    (Freer c fr, Union u, HFunctor (u ehs), HasMembershipRec u e r) =>
     Eff u fr ehs (e ': r) ~> Eff u fr ehs r
-subsume = transformAll $ inject |+: id
+subsume = transformAll $ injectRec |+: id
 {-# INLINE subsume #-}
 
 subsumeH ::
     forall e r efs fr u c.
-    (Freer c fr, Union u, HFunctor (u (e ': r)), HasMembership u e r) =>
+    (Freer c fr, Union u, HFunctor (u (e ': r)), HasMembershipRec u e r) =>
     Eff u fr (e ': r) efs ~> Eff u fr r efs
-subsumeH = transformAllH $ inject |+: id
+subsumeH = transformAllH $ injectRec |+: id
 {-# INLINE subsumeH #-}
 
+copyEff ::
+    forall e r ehs fr u c.
+    ( Freer c fr
+    , Union u
+    , HFunctor (u ehs)
+    , Applicative (Eff u fr ehs (e ': r))
+    , HeadIns e
+    , HasMembershipRec u e r
+    ) =>
+    Eff u fr ehs (e ': r) ~> Eff u fr ehs (e ': r)
+copyEff = reinterpretRec \e ->
+    send0 e *> liftEff (weaken $ injectRec $ liftInsIfSingle @_ @e e)
+
+copyEffH ::
+    forall e r ef fr u c.
+    ( Freer c fr
+    , Union u
+    , HFunctorUnion u
+    , HFunctor e
+    , ForallHFunctor u r
+    , Applicative (Eff u fr (e ': r) ef)
+    , HasMembershipRec u e r
+    ) =>
+    Eff u fr (e ': r) ef ~> Eff u fr (e ': r) ef
+copyEffH = reinterpretRecH \e -> send0H e *> liftEffH (weaken $ injectRec e)
+
+dupEff ::
+    forall e r ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs), Applicative (Eff u fr ehs (e ': e ': r)), HeadIns e) =>
+    Eff u fr ehs (e ': r) ~> Eff u fr ehs (e ': e ': r)
+dupEff = raiseUnder >>> reinterpretRec \e -> send0 e *> send1 e
+{-# INLINE dupEff #-}
+
+dupEffH ::
+    forall e r ef fr u c.
+    ( Freer c fr
+    , Union u
+    , Applicative (Eff u fr (e ': e ': r) ef)
+    , HFunctorUnion u
+    , HFunctor e
+    , ForallHFunctor u r
+    ) =>
+    Eff u fr (e ': r) ef ~> Eff u fr (e ': e ': r) ef
+dupEffH = raiseUnderH >>> reinterpretRecH \e -> send0H e *> send1H e
+{-# INLINE dupEffH #-}
+
+bundle ::
+    forall e r ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs)) =>
+    Eff u fr ehs (e ': r) ~> Eff u fr ehs (u '[e] ': r)
+bundle = transformAll $ inject0 . inject0 |+: weaken
+
+unbundle ::
+    forall e r ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs)) =>
+    Eff u fr ehs (u '[e] ': r) ~> Eff u fr ehs (e ': r)
+unbundle = transformAll $ inject0 . (id |+: end) |+: weaken
+
+pushBundle ::
+    forall e r1 r2 ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs)) =>
+    Eff u fr ehs (u r1 ': e ': r2) ~> Eff u fr ehs (u (e ': r1) ': r2)
+pushBundle = transformAll $ inject0 . weaken |+: inject0 . inject0 |+: weaken
+
+popBundle ::
+    forall e r1 r2 ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs)) =>
+    Eff u fr ehs (u (e ': r1) ': r2) ~> Eff u fr ehs (u r1 ': e ': r2)
+popBundle = transformAll $ (weaken . inject0 |+: inject0) |+: weaken2
+
+enqueSum ::
+    forall e1 e2 r ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs)) =>
+    Eff u fr ehs (e1 ': e2 ': r) ~> Eff u fr ehs (e1 :+: e2 ': r)
+enqueSum = transformAll $ inject0 . Inl |+: inject0 . Inr |+: weaken
+
+dequeSum ::
+    forall e1 e2 r ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs)) =>
+    Eff u fr ehs (e1 :+: e2 ': r) ~> Eff u fr ehs (e1 ': e2 ': r)
+dequeSum = transformAll $ caseH inject0 (weaken . inject0) |+: weaken2
+
 liftInsEff ::
     forall e eh ef fr u c.
     (Freer c fr, Union u, HFunctor (u eh), HFunctor e) =>
@@ -1028,21 +1198,29 @@
         . unHefty
 
 send0 :: (Freer c fr, Union u, HeadIns e) => UnliftIfSingle e ~> Eff u fr eh (e ': r)
-send0 = Hefty . liftIns . EffUnion . R1 . inject0 . liftInsIfSingle
+send0 = liftEff . inject0 . liftInsIfSingle
 {-# INLINE send0 #-}
 
 send1 :: (Freer c fr, Union u, HeadIns e1) => UnliftIfSingle e1 ~> Eff u fr eh (e2 ': e1 ': r)
-send1 = Hefty . liftIns . EffUnion . R1 . weaken . inject0 . liftInsIfSingle
+send1 = liftEff . weaken . inject0 . liftInsIfSingle
 {-# INLINE send1 #-}
 
 send0H :: (Freer c fr, Union u) => e (Eff u fr (e ': r) ef) ~> Eff u fr (e ': r) ef
-send0H = Hefty . liftIns . EffUnion . L1 . inject0
+send0H = liftEffH . inject0
 {-# INLINE send0H #-}
 
 send1H :: (Freer c fr, Union u) => e1 (Eff u fr (e2 ': e1 ': r) ef) ~> Eff u fr (e2 ': e1 ': r) ef
-send1H = Hefty . liftIns . EffUnion . L1 . weaken . inject0
+send1H = liftEffH . weaken . inject0
 {-# INLINE send1H #-}
 
+liftEff :: (Freer c fr, Union u) => u ef Nop ~> Eff u fr eh ef
+liftEff = Hefty . liftIns . EffUnion . R1
+{-# INLINE liftEff #-}
+
+liftEffH :: (Freer c fr, Union u) => u eh (Eff u fr eh ef) ~> Eff u fr eh ef
+liftEffH = Hefty . liftIns . EffUnion . L1
+{-# INLINE liftEffH #-}
+
 runEff :: forall f fr u c. (Freer c fr, Union u, c f) => Eff u fr '[] '[LiftIns f] ~> f
 runEff = interpretAll $ id |+ exhaust
 {-# INLINE runEff #-}
@@ -1050,6 +1228,20 @@
 runPure :: forall a fr u c. (Freer c fr, Union u, c Identity) => Eff u fr '[] '[] a -> a
 runPure = runIdentity . interpretAll exhaust
 {-# INLINE runPure #-}
+
+tagEff ::
+    forall tag e r ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs)) =>
+    Eff u fr ehs (LiftIns e ': r) ~> Eff u fr ehs (LiftIns (e # tag) ': r)
+tagEff = transform Tag
+{-# INLINE tagEff #-}
+
+tagEffH ::
+    forall tag e r efs fr u c.
+    (Freer c fr, Union u, HFunctor (u (e ': r))) =>
+    Eff u fr (e ': r) efs ~> Eff u fr (e ## tag ': r) efs
+tagEffH = transformH TagH
+{-# INLINE tagEffH #-}
 
 untagEff ::
     forall tag e r ehs fr u c.
diff --git a/src/Data/Hefty/Extensible.hs b/src/Data/Hefty/Extensible.hs
--- a/src/Data/Hefty/Extensible.hs
+++ b/src/Data/Hefty/Extensible.hs
@@ -20,6 +20,8 @@
     Forall,
 ) where
 
+import Control.Effect.Free qualified as E
+import Control.Effect.Hefty qualified as E
 import Data.Effect (SigClass)
 import Data.Effect.HFunctor (HFunctor, hfmap)
 import Data.Extensible (Forall, Match (Match), htabulateFor, match)
@@ -125,3 +127,6 @@
 
 type S ef = Union.S ExtensibleUnion ef
 type SH eh = Union.SH ExtensibleUnion eh
+
+type Eff fr eh ef = E.Eff ExtensibleUnion fr eh ef
+type EffF fr es = E.EffF ExtensibleUnion fr es
diff --git a/src/Data/Hefty/Union/Strengthen.hs b/src/Data/Hefty/Union/Strengthen.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Hefty/Union/Strengthen.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- This Source Code Form is subject to the terms of the Mozilla Public
+-- License, v. 2.0. If a copy of the MPL was not distributed with this
+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+
+{- |
+Copyright   :  (c) 2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+-}
+module Data.Hefty.Union.Strengthen where
+
+import Control.Effect (type (~>))
+import Data.Hefty.Union (MemberRec, Union (inject0, (|+:)), injectRec, weaken)
+import Data.Type.Equality (type (==))
+import GHC.TypeNats (Natural, type (-))
+
+class
+    (Union u, isMZero ~ (m == 0), isNZero ~ (n == 0)) =>
+    StrengthenUnder_ (isMZero :: Bool) (m :: Natural) (isNZero :: Bool) (n :: Natural) u es es'
+        | m n es -> es'
+    where
+    strengthenNUnderM_ :: u es f ~> u es' f
+
+type StrengthenUnder n m = StrengthenUnder_ (m == 0) m (n == 0) n
+type Strengthen n = StrengthenUnder_ 'True 0 (n == 0) n
+
+strengthenNUnderM :: forall n m u es' f es. StrengthenUnder n m u es es' => u es f ~> u es' f
+strengthenNUnderM = strengthenNUnderM_ @(m == 0) @m @(n == 0) @n
+{-# INLINE strengthenNUnderM #-}
+
+strengthenN :: forall n u es' f es. Strengthen n u es es' => u es f ~> u es' f
+strengthenN = strengthenNUnderM_ @( 'True) @0 @(n == 0) @n
+{-# INLINE strengthenN #-}
+
+instance
+    (Union u, StrengthenUnder n (m - 1) u es es', (m == 0) ~ 'False, isNZero ~ (n == 0)) =>
+    StrengthenUnder_ 'False m isNZero n u (e ': es) (e ': es')
+    where
+    strengthenNUnderM_ = inject0 |+: weaken . strengthenNUnderM @n @(m - 1)
+    {-# INLINE strengthenNUnderM_ #-}
+
+instance
+    (Union u, Strengthen (n - 1) u es es', MemberRec u e es, (n == 0) ~ 'False) =>
+    StrengthenUnder_ 'True 0 'False n u (e ': es) es'
+    where
+    strengthenNUnderM_ = strengthenN @(n - 1) . (injectRec |+: id)
+    {-# INLINE strengthenNUnderM_ #-}
+
+instance Union u => StrengthenUnder_ 'True 0 'True 0 u es es where
+    strengthenNUnderM_ = id
+    {-# INLINE strengthenNUnderM_ #-}
diff --git a/src/Data/Hefty/Union/Weaken.hs b/src/Data/Hefty/Union/Weaken.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Hefty/Union/Weaken.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- This Source Code Form is subject to the terms of the Mozilla Public
+-- License, v. 2.0. If a copy of the MPL was not distributed with this
+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+
+{- |
+Copyright   :  (c) 2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+-}
+module Data.Hefty.Union.Weaken where
+
+import Control.Effect (type (~>))
+import Data.Hefty.Union (Union (inject0, weaken, (|+:)))
+import Data.Type.Equality (type (==))
+import GHC.TypeNats (Natural, type (-))
+
+class
+    (isMZero ~ (m == 0), isNZero ~ (n == 0)) =>
+    WeakenUnder_ (isMZero :: Bool) (m :: Natural) (isNZero :: Bool) (n :: Natural) es es'
+        | m n es' -> es
+    where
+    weakenNUnderM_ :: Union u => u es f ~> u es' f
+
+type WeakenUnder n m = WeakenUnder_ (m == 0) m (n == 0) n
+type Weaken n = WeakenUnder_ 'True 0 (n == 0) n
+
+weakenNUnderM :: forall n m u es' f es. (Union u, WeakenUnder n m es es') => u es f ~> u es' f
+weakenNUnderM = weakenNUnderM_ @(m == 0) @m @(n == 0) @n
+{-# INLINE weakenNUnderM #-}
+
+weakenN :: forall n u es' f es. (Union u, Weaken n es es') => u es f ~> u es' f
+weakenN = weakenNUnderM_ @( 'True) @0 @(n == 0) @n
+{-# INLINE weakenN #-}
+
+instance
+    (WeakenUnder n (m - 1) es es', (m == 0) ~ 'False, isNZero ~ (n == 0)) =>
+    WeakenUnder_ 'False m isNZero n (e ': es) (e ': es')
+    where
+    weakenNUnderM_ = inject0 |+: weaken . weakenNUnderM @n @(m - 1)
+    {-# INLINE weakenNUnderM_ #-}
+
+instance
+    (Weaken (n - 1) es es', (n == 0) ~ 'False) =>
+    WeakenUnder_ 'True 0 'False n es (e ': es')
+    where
+    weakenNUnderM_ = weaken . weakenN @(n - 1)
+    {-# INLINE weakenNUnderM_ #-}
+
+instance WeakenUnder_ 'True 0 'True 0 es es where
+    weakenNUnderM_ = id
+    {-# INLINE weakenNUnderM_ #-}