diff --git a/debruijn-safe.cabal b/debruijn-safe.cabal
--- a/debruijn-safe.cabal
+++ b/debruijn-safe.cabal
@@ -1,6 +1,6 @@
 cabal-version: 2.4
 name:          debruijn-safe
-version:       0.2
+version:       0.3
 license:       BSD-3-Clause
 license-file:  LICENSE
 category:      Development
diff --git a/src-common/DeBruijn/Ren.hs b/src-common/DeBruijn/Ren.hs
--- a/src-common/DeBruijn/Ren.hs
+++ b/src-common/DeBruijn/Ren.hs
@@ -10,24 +10,18 @@
     -- ** Category
     idRen,
     compRen,
-    -- * Applicative renamings
-    RenA (..),
-    renameIdxA,
-    keepRenA,
+    -- * Contractions
     unusedIdx,
     -- * Renameble things
-    IdxMapping (..),
+    Keep (..),
     keepAdd,
     Weaken (..),
+    Contract (..),
     Rename (..),
-    RenameA (..),
-    defaultRename,
-    defaultWeaken,
 ) where
 
-import Data.Functor.Identity (Identity (..))
-import Data.Kind             (Constraint, Type)
-import Data.Proxy            (Proxy (..))
+import Data.Kind  (Constraint, Type)
+import Data.Proxy (Proxy (..))
 
 import DeBruijn.Add
 import DeBruijn.Ctx
@@ -36,8 +30,6 @@
 import DeBruijn.Size
 import DeBruijn.Wk
 
-import TrustworthyCompat (coerce)
-
 -------------------------------------------------------------------------------
 -- Renamings
 -------------------------------------------------------------------------------
@@ -88,39 +80,22 @@
 -- Applicative renamings
 -------------------------------------------------------------------------------
 
-type RenA :: (Type -> Type) -> Ctx -> Ctx -> Type
-newtype RenA f ctx ctx' = MkRenA (Env ctx (f (Idx ctx')))
-
--- | Lift renaming (used when going under a binder).
-keepRenA :: Applicative f => RenA f ctx ctx' -> RenA f (S ctx) (S ctx')
-keepRenA (MkRenA js) = MkRenA (fmap (fmap IS) js :> pure IZ)
-
-unusedIdx :: Size ctx -> RenA Maybe (S ctx) ctx
-unusedIdx s = MkRenA $ tabulateEnv (SS s) $ unIdx Nothing Just
+unusedIdx :: Wk ctx (S ctx)
+unusedIdx = wk1
 
 -------------------------------------------------------------------------------
 -- Renameble & RenamebleA
 -------------------------------------------------------------------------------
 
--- | 'IdxMapping' generalizes over various index mappings, also effectful ones.
-type IdxMapping :: (Type -> Type) -> (Ctx -> Ctx -> Type) -> Constraint
-class Applicative f => IdxMapping f t | t -> f where
-    -- | 'IdxMapping' action.
-    mapIdx :: t ctx ctx' -> Idx ctx -> f (Idx ctx')
-
+type Keep :: (Ctx -> Ctx -> Type) -> Constraint
+class Keep t where
     -- | 'keep' is often called @lift@, but we stick with 'Wk' terminology.
     -- One benefit is that the name 'keep' is less likely to clash.
     keep   :: t ctx ctx' -> t (S ctx) (S ctx')
 
-    -- | Compose weakening with an index mapping.
-    --
-    -- This is useful when you have explicit weakening in your terms.
-    -- (a similar idea as in @bound@'s @Scope@ possibly lifting whole term).
-    weakenIdxMapping :: Wk ctx ctx' -> t ctx' ctx'' -> t ctx ctx''
-
 -- | 'keep' 'IdxMapping' @arity@ times.
 keepAdd
-    :: IdxMapping f m
+    :: Keep m
     => Add arity ctxA ctxA'
     -> m ctxA ctxB
     -> (forall ctxB'. Add arity ctxB ctxB' -> m ctxA' ctxB' -> r)
@@ -128,24 +103,12 @@
 keepAdd AZ     w kont = kont AZ w
 keepAdd (AS a) w kont = keepAdd a w $ \a' w' -> kont (AS a') (keep w')
 
-instance IdxMapping Identity Wk where
+instance Keep Wk where
     keep = KeepWk
-    mapIdx w x = Identity (weakenIdx w x)
-    weakenIdxMapping = compWk
 
-instance IdxMapping Identity Ren where
+instance Keep Ren where
     keep = keepRen
-    mapIdx w x = Identity (renameIdx w x)
-    weakenIdxMapping w (MkRen is) = MkRen (weakenEnv w is)
 
-instance Applicative f => IdxMapping f (RenA f) where
-    keep = keepRenA
-    mapIdx = renameIdxA
-    weakenIdxMapping w (MkRenA is) = MkRenA (weakenEnv w is)
-
-renameIdxA :: RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')
-renameIdxA (MkRenA js) i = lookupEnv i js
-
 -- | Renameble things.
 --
 -- For most terms it's enough to define a single traversal: an instance of 'RenamebleA' type-class,
@@ -161,28 +124,9 @@
 class Weaken t => Rename t where
     rename :: Ren n m -> t n -> t m
 
--- | 'rename' implementation using 'grename'.
-defaultRename :: forall t n m. RenameA t => Ren n m -> t n -> t m
-defaultRename = coerce (grename @t @Ren @Identity @n @m)
-
--- | 'weaken' implementation using 'grename'.
-defaultWeaken :: forall t n m. RenameA t => Wk n m -> t n -> t m
-defaultWeaken = coerce (grename @t @Wk @Identity @n @m)
-
--- | Effectful renamings.
---
--- An common example is checking whether a binding is used:
---
--- @
--- Just t' <- 'renameA' 'unusedIdx' t
--- @
---
-class Rename t => RenameA t where
-    renameA :: forall f ctx ctx'. Applicative f => RenA f ctx ctx' -> t ctx -> f (t ctx')
-    renameA = grename
-
-    -- | Generic renaming of a term @t@ using any 'IdxMapping'.
-    grename :: forall m f ctx ctx'. IdxMapping f m => m ctx ctx' -> t ctx -> f (t ctx')
+-- | Contractions
+class Contract t where
+    contract :: Wk m n -> t n -> Maybe (t m)
 
 instance Weaken Proxy where
      weaken _ _ = Proxy
@@ -190,8 +134,8 @@
 instance Rename Proxy where
     rename _ _ = Proxy
 
-instance RenameA Proxy where
-    grename _ _ = pure Proxy
+instance Contract Proxy where
+    contract _ _ = Just Proxy
 
 instance Weaken Idx where
     weaken = weakenIdx
@@ -199,8 +143,8 @@
 instance Rename Idx where
     rename = renameIdx
 
-instance RenameA Idx where
-    grename = mapIdx
+instance Contract Idx where
+    contract = contractIdx
 
 instance Weaken (Ren n) where
     weaken w (MkRen js) = MkRen (fmap (weaken w) js)
diff --git a/src-common/DeBruijn/Sub.hs b/src-common/DeBruijn/Sub.hs
--- a/src-common/DeBruijn/Sub.hs
+++ b/src-common/DeBruijn/Sub.hs
@@ -45,7 +45,7 @@
 snocSub :: Sub t ctx ctx' -> t ctx' -> Sub t (S ctx) ctx'
 snocSub (MkSub s) t = MkSub (s :> t)
 
-keepSub :: (Rename t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx')
+keepSub :: (Weaken t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx')
 keepSub (MkSub ts) = MkSub (fmap (weaken wk1) ts :> var IZ)
 
 -- | Precompose 'Sub' with weakening.
@@ -53,7 +53,7 @@
 weakenSub w (MkSub ts) = MkSub (weakenEnv w ts)
 
 -- TODO:
-nameMe :: Rename t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx''
+nameMe :: Weaken t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx''
 nameMe (MkSub ts) w = MkSub (fmap (weaken w) ts)
 
 -------------------------------------------------------------------------------
diff --git a/src/DeBruijn/RenExtras.hs b/src/DeBruijn/RenExtras.hs
--- a/src/DeBruijn/RenExtras.hs
+++ b/src/DeBruijn/RenExtras.hs
@@ -11,7 +11,7 @@
 -- | Weaken closed term to arbitrary context.
 --
 -- Note: this has different requirements than 'sinkSize'.
-weakenUsingSize :: Rename t => Size ctx -> t EmptyCtx -> t ctx
+weakenUsingSize :: Weaken t => Size ctx -> t EmptyCtx -> t ctx
 weakenUsingSize s0 = weaken (go s0) where
     go :: Size ctx -> Wk EmptyCtx ctx
     go SZ     = IdWk