diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,6 @@
+0.1.2
+  * Add subst2. Thanks to James Koppel.
+
 0.1.1
   * Turn on PolyKinds for GHC >= 7.6. Thanks to Ben Franksen.
 
diff --git a/src/Data/Type/Equality.hs b/src/Data/Type/Equality.hs
--- a/src/Data/Type/Equality.hs
+++ b/src/Data/Type/Equality.hs
@@ -23,6 +23,7 @@
   , sym
   , trans
   , subst
+  , subst2
   
   , cong
   , cong2
@@ -79,6 +80,11 @@
 -- be defined as 'coerce' '.' 'cong'.
 subst :: a :=: b -> f a -> f b
 subst Refl = id
+
+-- | Substitution inside nested type constructors. This is equivalent 
+-- to 'coerce' '.' 'cong' '.' 'cong'.
+subst2 :: a :=: b -> f (g a) -> f (g b)
+subst2 Refl = id
 
 -- | Equality is congruential.
 cong :: a :=: b -> f a :=: f b
diff --git a/type-equality.cabal b/type-equality.cabal
--- a/type-equality.cabal
+++ b/type-equality.cabal
@@ -1,5 +1,5 @@
 Name:                type-equality
-Version:             0.1.1
+Version:             0.1.2
 Synopsis:            Type equality, coercion/cast and other operations.
 Description:         In the presence of GADTs, sometimes a proof is
                      needed that two types are equal. This package