diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,10 @@
+## 0.3 [2017-11-07]
+* Migrate the old `elimNat` from `Data.Eliminator` (which worked over the `Nat`
+  from `GHC.TypeNats`) to `Data.Eliminator.TypeNats`. There `elimNat` that now
+  lives in `Data.Eliminator` is for an unrelated `Nat` data type from the
+  `singleton-nats` package (which is a proper, inductively defined, Peano
+  natural number type).
+
 ## 0.2 [2017-07-22]
 * Introduce the `Data.Eliminator.TH` module, which provides functionality for
   generating eliminator functions using Template Haskell. Currently, only
diff --git a/eliminators.cabal b/eliminators.cabal
--- a/eliminators.cabal
+++ b/eliminators.cabal
@@ -1,5 +1,5 @@
 name:                eliminators
-version:             0.2
+version:             0.3
 synopsis:            Dependently typed elimination functions using singletons
 description:         This library provides eliminators for inductive data types,
                      leveraging the power of the @singletons@ library to allow
@@ -25,12 +25,14 @@
 library
   exposed-modules:     Data.Eliminator
                        Data.Eliminator.TH
-  build-depends:       base             >= 4.10  && < 4.11
-                     , extra            >= 1.4.2 && < 1.7
-                     , singletons       >= 2.3   && < 2.4
-                     , template-haskell >= 2.12  && < 2.13
-                     , th-abstraction   >= 0.2.3 && < 0.3
-                     , th-desugar       >= 1.7   && < 1.8
+                       Data.Eliminator.TypeNats
+  build-depends:       base             >= 4.10    && < 4.11
+                     , extra            >= 1.4.2   && < 1.7
+                     , singletons       >= 2.3     && < 2.4
+                     , singleton-nats   >= 0.4.0.3 && < 0.5
+                     , template-haskell >= 2.12    && < 2.13
+                     , th-abstraction   >= 0.2.3   && < 0.3
+                     , th-desugar       >= 1.7     && < 1.8
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall -Wno-unticked-promoted-constructors
@@ -38,17 +40,19 @@
 test-suite spec
   type:                exitcode-stdio-1.0
   main-is:             Spec.hs
-  other-modules:       EqualitySpec
+  other-modules:       DecideSpec
+                       DecideTypes
+                       EqualitySpec
                        GADTSpec
                        ListSpec
                        ListTypes
-                       PeanoSpec
-                       PeanoTypes
+                       VecTypes
                        VecSpec
-  build-depends:       base       >= 4.10 && < 4.11
+  build-depends:       base           >= 4.10    && < 4.11
                      , eliminators
-                     , hspec      >= 2    && < 3
-                     , singletons >= 2.3  && < 2.4
+                     , hspec          >= 2       && < 3
+                     , singletons     >= 2.3     && < 2.4
+                     , singleton-nats >= 0.4.0.3 && < 0.5
   hs-source-dirs:      tests
   default-language:    Haskell2010
   ghc-options:         -Wall -Wno-unticked-promoted-constructors -threaded -rtsopts
diff --git a/src/Data/Eliminator.hs b/src/Data/Eliminator.hs
--- a/src/Data/Eliminator.hs
+++ b/src/Data/Eliminator.hs
@@ -39,20 +39,15 @@
   , elimTuple7
   ) where
 
-import           Control.Monad.Extra
-
-import           Data.Eliminator.TH
-import           Data.Kind (Type)
-import           Data.List.NonEmpty (NonEmpty(..))
-import           Data.Singletons.Prelude
-import           Data.Singletons.Prelude.List.NonEmpty (Sing(..))
-import           Data.Singletons.TypeLits
-
-import qualified GHC.TypeLits as TL
+import Control.Monad.Extra
 
-import           Language.Haskell.TH.Desugar (tupleNameDegree_maybe)
+import Data.Eliminator.TH
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Nat
+import Data.Singletons.Prelude
+import Data.Singletons.Prelude.List.NonEmpty (Sing(..))
 
-import           Unsafe.Coerce (unsafeCoerce)
+import Language.Haskell.TH.Desugar (tupleNameDegree_maybe)
 
 {- $eliminators
 
@@ -70,23 +65,8 @@
   with @~>@ prepended.
 -}
 
-$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''NonEmpty, ''Ordering])
+$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''Nat, ''NonEmpty, ''Ordering])
 $(deriveElimNamed "elimList" ''[])
 $(concatMapM (\n -> let Just deg = tupleNameDegree_maybe n
                     in deriveElimNamed ("elimTuple" ++ show deg) n)
              [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])
-
--- This is the grimy one we can't define using Template Haskell.
-
--- | Although 'Nat' is not actually an inductive data type in GHC, we can
--- pretend that it is using this eliminator.
-elimNat :: forall (p :: Nat ~> Type) (n :: Nat).
-           Sing n
-        -> p @@ 0
-        -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k TL.+ 1))
-        -> p @@ n
-elimNat snat pZ pS =
-  case fromSing snat of
-    0        -> unsafeCoerce pZ
-    nPlusOne -> withSomeSing (pred nPlusOne) $ \(sn :: Sing k) ->
-                  unsafeCoerce (pS sn (elimNat @p @k sn pZ pS))
diff --git a/src/Data/Eliminator/TH.hs b/src/Data/Eliminator/TH.hs
--- a/src/Data/Eliminator/TH.hs
+++ b/src/Data/Eliminator/TH.hs
@@ -53,7 +53,7 @@
            -> p '@@' l
 elimMyList SMyNil pMyNil _ = pMyNil
 elimMyList (SMyCons (x' :: 'Sing' x) (xs' :: 'Sing' xs)) pMyNil pMyCons
-  = pMyCons x' xs' (elimMyList @a @p @xs pMyNil pMyCons)
+  = pMyCons x' xs' (elimMyList \@a \@p \@xs pMyNil pMyCons)
 @
 
 There are some important things to note here:
diff --git a/src/Data/Eliminator/TypeNats.hs b/src/Data/Eliminator/TypeNats.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Eliminator/TypeNats.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-|
+Module:      Data.Eliminator.TypeNats
+Copyright:   (C) 2017 Ryan Scott
+License:     BSD-style (see the file LICENSE)
+Maintainer:  Ryan Scott
+Stability:   Experimental
+Portability: GHC
+
+A crude imitation of an eliminator function for 'GHC.TypeNats.Nat'.
+-}
+module Data.Eliminator.TypeNats (elimNat) where
+
+import Data.Kind (Type)
+import Data.Singletons
+import Data.Singletons.TypeLits
+
+import GHC.TypeNats
+
+import Unsafe.Coerce (unsafeCoerce)
+
+-- | Although 'Nat' is not actually an inductive data type in GHC, we can
+-- (crudely) pretend that it is using this eliminator.
+elimNat :: forall (p :: Nat ~> Type) (n :: Nat).
+           Sing n
+        -> p @@ 0
+        -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k + 1))
+        -> p @@ n
+elimNat snat pZ pS =
+  case fromSing snat of
+    0        -> unsafeCoerce pZ
+    nPlusOne -> withSomeSing (pred nPlusOne) $ \(sn :: Sing k) ->
+                  unsafeCoerce (pS sn (elimNat @p @k sn pZ pS))
diff --git a/tests/DecideSpec.hs b/tests/DecideSpec.hs
new file mode 100644
--- /dev/null
+++ b/tests/DecideSpec.hs
@@ -0,0 +1,222 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module DecideSpec where
+
+import Data.Eliminator
+import Data.Nat
+import Data.Singletons.Prelude
+import Data.Singletons.TH hiding (Decision(..))
+import Data.Type.Equality
+
+import EqualitySpec (cong, replace)
+import DecideTypes
+
+import Test.Hspec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = parallel $ do
+  let proved    = "Proved Refl"
+      disproved = "Disproved <void>"
+  describe "decEqNat" $ do
+    it "returns evidence that two Nats are equal" $ do
+      show (decEqNat (sLit @0) (sLit @0)) `shouldBe` proved
+      show (decEqNat (sLit @1) (sLit @0)) `shouldBe` disproved
+      show (decEqNat (sLit @0) (sLit @1)) `shouldBe` disproved
+      show (decEqNat (sLit @1) (sLit @1)) `shouldBe` proved
+  describe "decEqList" $ do
+    it "returns evidence that two lists are equal" $ do
+      let decEqNatList = decEqList decEqNat
+      show (decEqNatList SNil                   SNil)                   `shouldBe` proved
+      show (decEqNatList (SCons (sLit @0) SNil) SNil)                   `shouldBe` disproved
+      show (decEqNatList SNil                   (SCons (sLit @0) SNil)) `shouldBe` disproved
+      show (decEqNatList (SCons (sLit @0) SNil) (SCons (sLit @0) SNil)) `shouldBe` proved
+      -- TODO: Try this in the next version of singletons
+      -- show (decEqNatList (SCons (sLit @1) SNil) (SCons (sLit @0) SNil)) `shouldBe` disproved
+
+-----
+
+peanoEqConsequencesSame :: forall (n :: Nat). Sing n -> NatEqConsequences n n
+peanoEqConsequencesSame sn = elimNat @WhyNatEqConsequencesSameSym0 @n sn base step
+  where
+    base :: WhyNatEqConsequencesSame Z
+    base = ()
+
+    step :: forall (k :: Nat).
+            Sing k
+         -> WhyNatEqConsequencesSame k
+         -> WhyNatEqConsequencesSame (S k)
+    step _ _ = Refl
+
+useNatEq :: forall n j. Sing n -> n :~: j -> NatEqConsequences n j
+useNatEq sn nEqJ = replace @Nat @n @j @(NatEqConsequencesSym1 n)
+                             (peanoEqConsequencesSame @n sn) nEqJ
+
+zNotS :: forall n. Z :~: S n -> Void
+zNotS = useNatEq @Z @(S n) SZ
+
+sNotZ :: forall n. S n :~: Z -> Void
+sNotZ eq = zNotS @n (sym eq)
+
+sInjective :: forall n j. Sing n -> S n :~: S j -> n :~: j
+sInjective sn = useNatEq @(S n) @(S j) (SS sn)
+
+decEqZ :: forall (j :: Nat). Sing j -> Decision (Z :~: j)
+decEqZ sj = elimNat @WhyDecEqZSym0 @j sj base step
+  where
+    base :: Decision (Z :~: Z)
+    base = Proved Refl
+
+    step :: forall (k :: Nat).
+            Sing k -> Decision (Z :~: k) -> Decision (Z :~: S k)
+    step _ _ = Disproved (zNotS @k)
+
+decCongS :: forall n j. Sing n -> Decision (n :~: j) -> Decision (S n :~: S j)
+decCongS sn dNJ = withSomeSing dNJ $ \(sDNJ :: Sing d) ->
+                    elimDecision @_ @(ConstSym1 (Decision (S n :~: S j))) @d
+                      sDNJ left right
+  where
+    left :: forall (x :: n :~: j).
+            Sing x -> Decision (S n :~: S j)
+    left yes = Proved $ cong @Nat @Nat @(TyCon1 S) @n @j (fromSing yes)
+
+    right :: forall (r :: (n :~: j) ~> Void).
+             Sing r -> Decision (S n :~: S j)
+    right no = Disproved $ fromSing no . sInjective @n @j sn
+
+decEqNat :: forall (n :: Nat) (j :: Nat). Sing n -> Sing j -> Decision (n :~: j)
+decEqNat sn = runWhyDecEqNat (elimNat @(TyCon1 WhyDecEqNat) @n sn base step)
+  where
+    base :: WhyDecEqNat Z
+    base = WhyDecEqNat decEqZ
+
+    step :: forall (k :: Nat).
+            Sing k
+         -> WhyDecEqNat k
+         -> WhyDecEqNat (S k)
+    step sk swhyK = WhyDecEqNat $ \(sl :: Sing l) ->
+                      elimNat @(WhyDecEqSSym1 k) @l sl baseStep stepStep
+      where
+        baseStep :: Decision (S k :~: Z)
+        baseStep = Disproved $ sNotZ @k
+
+        stepStep :: forall (m :: Nat).
+                    Sing m
+                 -> Decision (S k :~: m)
+                 -> Decision (S k :~: S m)
+        stepStep sm _ = decCongS sk (runWhyDecEqNat swhyK sm)
+
+listEqConsequencesSame :: forall (es :: [e]). Sing es -> ListEqConsequences es es
+listEqConsequencesSame sl = elimList @e @WhyListEqConsequencesSameSym0 @es sl base step
+  where
+    base :: ListEqConsequences '[] '[]
+    base = ()
+
+    step :: forall (x :: e) (xs :: [e]).
+            Sing x -> Sing xs
+         -> ListEqConsequences xs xs
+         -> ListEqConsequences (x:xs) (x:xs)
+    step _ _ _ = (Refl, Refl)
+
+useListEq :: forall (xs :: [e]) (ys :: [e]).
+             Sing xs -> xs :~: ys -> ListEqConsequences xs ys
+useListEq sxs xsEqYs = replace @[e] @xs @ys @(ListEqConsequencesSym1 xs)
+                               (listEqConsequencesSame @e @xs sxs) xsEqYs
+
+nilNotCons :: forall (x :: e) (xs :: [e]). '[] :~: (x:xs) -> Void
+nilNotCons = useListEq @e @'[] @(x:xs) SNil
+
+consNotNil :: forall (x :: e) (xs :: [e]). (x:xs) :~: '[] -> Void
+consNotNil eq = nilNotCons @e @x @xs (sym eq)
+
+consInjective :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).
+                 Sing x -> Sing xs
+              -> (x:xs) :~: (y:ys)
+              -> (x :~: y, xs :~: ys)
+consInjective sx sxs = useListEq @e @(x:xs) @(y:ys) (SCons sx sxs)
+
+decEqNil :: forall (es :: [e]). Sing es -> Decision ('[] :~: es)
+decEqNil ses = elimList @e @WhyDecEqNilSym0 @es ses base step
+  where
+    base :: Decision ('[] :~: '[])
+    base = Proved Refl
+
+    step :: forall (x :: e) (xs :: [e]).
+            Sing x -> Sing xs
+         -> Decision ('[] :~: xs)
+         -> Decision ('[] :~: (x:xs))
+    step _ _ _ = Disproved (nilNotCons @e @x @xs)
+
+intermixListEqs :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).
+                   x :~: y -> xs :~: ys
+                -> (x:xs) :~: (y:ys)
+intermixListEqs xEqY xsEqYs =
+  replace @e @x @y @(WhyIntermixListEqs1Sym3 x xs ys)
+          (replace @[e] @xs @ys @(WhyIntermixListEqs2Sym2 x xs) Refl xsEqYs)
+          xEqY
+
+decCongCons :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).
+               Sing x -> Sing xs
+            -> Decision (x :~: y) -> Decision (xs :~: ys)
+            -> Decision ((x:xs) :~: (y:ys))
+decCongCons sx sxs dXY dXsYs =
+  withSomeSing dXY $ \(sDXY :: Sing dXY) ->
+    elimDecision @_ @(ConstSym1 (Decision ((x:xs) :~: (y:ys)))) @dXY
+      sDXY left right
+  where
+    left :: forall (z :: x :~: y).
+            Sing z -> Decision ((x:xs) :~: (y:ys))
+    left xEqY = withSomeSing dXsYs $ \(sDXsYs :: Sing dXsYs) ->
+                  elimDecision @_ @(ConstSym1 (Decision ((x:xs) :~: (y:ys)))) @dXsYs
+                    sDXsYs leftLeft leftRight
+      where
+        leftLeft :: forall (zz :: xs :~: ys).
+                    Sing zz -> Decision ((x:xs) :~: (y:ys))
+        leftLeft xsEqYs = Proved $ intermixListEqs (fromSing xEqY) (fromSing xsEqYs)
+
+        leftRight :: forall (r :: (xs :~: ys) ~> Void).
+                     Sing r -> Decision ((x:xs) :~: (y:ys))
+        leftRight no = Disproved $ fromSing no . snd . injective
+
+    right :: forall (r :: (x :~: y) ~> Void).
+             Sing r -> Decision ((x:xs) :~: (y:ys))
+    right no = Disproved $ fromSing no . fst . injective
+
+    injective :: (x:xs) :~: (y:ys) -> (x :~: y, xs :~: ys)
+    injective = consInjective @e @x @xs @y @ys sx sxs
+
+decEqList :: forall (es1 :: [e]) (es2 :: [e]).
+             (forall (e1 :: e) (e2 :: e).
+                     Sing e1 -> Sing e2 -> Decision (e1 :~: e2))
+          -> Sing es1 -> Sing es2 -> Decision (es1 :~: es2)
+decEqList f ses1 = runWhyDecEqList (elimList @e @(TyCon1 WhyDecEqList) @es1 ses1 base step)
+  where
+    base :: WhyDecEqList '[]
+    base = WhyDecEqList decEqNil
+
+    step :: forall (x :: e) (xs :: [e]).
+            Sing x -> Sing xs
+         -> WhyDecEqList xs
+         -> WhyDecEqList (x:xs)
+    step sx sxs swhyXs = WhyDecEqList $ \(sl :: Sing l) ->
+                           elimList @e @(WhyDecEqConsSym2 x xs) @l sl
+                             stepBase stepStep
+      where
+        stepBase :: Decision ((x:xs) :~: '[])
+        stepBase = Disproved $ consNotNil @e @x @xs
+
+        stepStep :: forall (y :: e) (ys :: [e]).
+                    Sing y -> Sing ys
+                 -> Decision ((x:xs) :~: ys)
+                 -> Decision ((x:xs) :~: (y:ys))
+        stepStep sy sys _ = decCongCons sx sxs
+                                        (f sx sy)
+                                        (runWhyDecEqList swhyXs sys)
diff --git a/tests/DecideTypes.hs b/tests/DecideTypes.hs
new file mode 100644
--- /dev/null
+++ b/tests/DecideTypes.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- TODO: Remove this in the next version of singletons
+{-# OPTIONS_GHC -Wno-orphans #-}
+module DecideTypes where
+
+import Data.Kind
+import Data.Nat
+import Data.Singletons.TH hiding (Decision(..))
+
+-- TODO: Remove these in the next version of singletons
+$(genSingletons [''Void])
+$(genDefunSymbols [''(~>)])
+
+-- Due to https://github.com/goldfirere/singletons/issues/82, promoting the
+-- Decision data type from Data.Singletons.Decide is a tad awkward. To work
+-- around these, we define a more general Decision' data type here.
+data Decision' p a
+  = Proved a
+  | Disproved (p @@ a @@ Void)
+
+elimDecision :: forall (a :: Type) (p :: PDecision a ~> Type) (d :: PDecision a).
+                Sing d
+             -> (forall (yes :: a). Sing yes -> p @@ (Proved yes))
+             -> (forall (no :: a ~> Void). Sing no -> p @@ (Disproved no))
+             -> p @@ d
+elimDecision (SProved yes)   pProved _          = pProved yes
+elimDecision (SDisproved no) _       pDisproved = pDisproved no
+
+instance Show a => Show (Decision' p a) where
+  showsPrec p (Proved a) =
+    showParen (p > 10) $ showString "Proved " . showsPrec 11 a
+  showsPrec p (Disproved _) =
+    showParen (p > 10) $ showString "Disproved <void>"
+
+type Decision  = Decision' (TyCon2 (->))
+type PDecision = Decision' (:~>$)
+
+data instance Sing (z :: PDecision a) where
+  -- It would be lovely to not have to write those (:: PDecision a) kind
+  -- ascriptions in the return types of each constructor.
+  -- See https://ghc.haskell.org/trac/ghc/ticket/14111.
+  SProved    :: forall (x :: a).         Sing x -> Sing (Proved x    :: PDecision a)
+  SDisproved :: forall (r :: a ~> Void). Sing r -> Sing (Disproved r :: PDecision a)
+
+instance SingKind a => SingKind (PDecision a) where
+  type Demote (PDecision a) = Decision (Demote a)
+  fromSing (SProved a)    = Proved (fromSing a)
+  fromSing (SDisproved r) = Disproved (fromSing r)
+  toSing (Proved x)    = withSomeSing x $ SomeSing . SProved
+  toSing (Disproved r) = withSomeSing r $ SomeSing . SDisproved
+
+type family NatEqConsequences (a :: Nat) (b :: Nat) :: Type where
+  NatEqConsequences Z      Z      = ()
+  NatEqConsequences Z      (S _)  = Void
+  NatEqConsequences (S _)  Z      = Void
+  NatEqConsequences (S k1) (S k2) = k1 :~: k2
+$(genDefunSymbols [''NatEqConsequences])
+
+type WhyNatEqConsequencesSame (a :: Nat) = NatEqConsequences a a
+$(genDefunSymbols [''WhyNatEqConsequencesSame])
+
+type WhyDecEqZ (k :: Nat) = Decision (Z :~: k)
+$(genDefunSymbols [''WhyDecEqZ])
+
+type WhyDecEqS (n :: Nat) (k :: Nat) = Decision (S n :~: k)
+$(genDefunSymbols [''WhyDecEqS])
+
+-- The newtype wrapper is needed to work around
+-- https://github.com/goldfirere/singletons/issues/198
+newtype WhyDecEqNat (k :: Nat) = WhyDecEqNat
+  { runWhyDecEqNat :: forall (j :: Nat). Sing j -> Decision (k :~: j) }
+
+type family ListEqConsequences (xxs :: [e]) (yys :: [e]) :: Type where
+  ListEqConsequences '[]    '[]    = ()
+  ListEqConsequences '[]    (_:_)  = Void
+  ListEqConsequences (_:_)  '[]    = Void
+  ListEqConsequences (x:xs) (y:ys) = (x :~: y, xs :~: ys)
+$(genDefunSymbols [''ListEqConsequences])
+
+type WhyListEqConsequencesSame (es :: [e]) = ListEqConsequences es es
+$(genDefunSymbols [''WhyListEqConsequencesSame])
+
+type WhyDecEqNil (es :: [e]) = Decision ('[] :~: es)
+$(genDefunSymbols [''WhyDecEqNil])
+
+type WhyDecEqCons (x :: e) (xs :: [e]) (es :: [e]) = Decision ((x:xs) :~: es)
+$(genDefunSymbols [''WhyDecEqCons])
+
+type WhyIntermixListEqs1 (x :: e) (xs :: [e]) (ys :: [e]) (k :: e) = (x:xs) :~: (k:ys)
+type WhyIntermixListEqs2 (x :: e) (xs :: [e]) (k :: [e])           = (x:xs) :~: (x:k)
+$(genDefunSymbols [''WhyIntermixListEqs1, ''WhyIntermixListEqs2])
+
+-- The newtype wrapper is needed to work around
+-- https://github.com/goldfirere/singletons/issues/198
+newtype WhyDecEqList (l1 :: [e]) = WhyDecEqList
+  { runWhyDecEqList :: forall (l2 :: [e]). Sing l2 -> Decision (l1 :~: l2) }
diff --git a/tests/EqualitySpec.hs b/tests/EqualitySpec.hs
--- a/tests/EqualitySpec.hs
+++ b/tests/EqualitySpec.hs
@@ -43,7 +43,9 @@
 instance SingI Refl where
   sing = SRefl
 
-(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).
+(~>:~:) :: forall (k :: Type) (a :: k) (b :: k)
+                  (p :: forall (y :: k). a :~: y ~> Type)
+                  (r :: a :~: b).
            Sing r
         -> p @@ Refl
         -> p @@ r
@@ -61,7 +63,9 @@
 instance SingI HRefl where
   sing = SHRefl
 
-(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y ~> Type).
+(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
+                   (p :: forall (z :: Type) (y :: z). a :~~: y ~> Type)
+                   (r :: a :~~: b).
             Sing r
          -> p @@ HRefl
          -> p @@ r
@@ -77,7 +81,7 @@
 sym :: forall (t :: Type) (a :: t) (b :: t).
        a :~: b -> b :~: a
 sym eq = withSomeSing eq $ \(singEq :: Sing r) ->
-           (~>:~:) @t @a @b @r @(WhySymSym a) singEq Refl
+           (~>:~:) @t @a @b @(WhySymSym a) @r singEq Refl
 
 type WhyHsym (a :: j) (y :: z) (e :: a :~~: y) = y :~~: a
 data WhyHsymSym (a :: j) :: forall (z :: Type) (y :: z). a :~~: y ~> Type
@@ -87,7 +91,7 @@
 hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).
         a :~~: b -> b :~~: a
 hsym eq = withSomeSing eq $ \(singEq :: Sing r) ->
-            (~>:~~:) @j @k @a @b @r @(WhyHsymSym a) singEq HRefl
+            (~>:~~:) @j @k @a @b @(WhyHsymSym a) @r singEq HRefl
 
 type family Symmetry (x :: (a :: k) :~: (b :: k)) :: b :~: a where
   Symmetry Refl = Refl
@@ -101,7 +105,7 @@
 symIdempotent :: forall (t :: Type) (a :: t) (b :: t)
                         (e :: a :~: b).
                  Sing e -> Symmetry (Symmetry e) :~: e
-symIdempotent se = (~>:~:) @t @a @b @e @(WhySymIdempotentSym a) se Refl
+symIdempotent se = (~>:~:) @t @a @b @(WhySymIdempotentSym a) @e se Refl
 
 type family Hsymmetry (x :: (a :: j) :~~: (b :: k)) :: b :~~: a where
   Hsymmetry HRefl = HRefl
@@ -115,7 +119,7 @@
 hsymIdempotent :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
                          (e :: a :~~: b).
                   Sing e -> Hsymmetry (Hsymmetry e) :~: e
-hsymIdempotent se = (~>:~~:) @j @k @a @b @e @(WhyHsymIdempotentSym a) se Refl
+hsymIdempotent se = (~>:~~:) @j @k @a @b @(WhyHsymIdempotentSym a) @e se Refl
 
 type WhyReplace (from :: t) (p :: t ~> Type)
                 (y :: t) (e :: from :~: y) = p @@ y
@@ -130,7 +134,7 @@
         -> p @@ to
 replace from eq =
   withSomeSing eq $ \(singEq :: Sing r) ->
-    (~>:~:) @t @from @to @r @(WhyReplaceSym from p) singEq from
+    (~>:~:) @t @from @to @(WhyReplaceSym from p) @r singEq from
 
 {-
 type WhyHreplace (from :: j) (p :: forall (z :: Type). z ~> Type)
@@ -175,4 +179,22 @@
      -> f @@ a :~: f @@ b
 cong eq =
   withSomeSing eq $ \(singEq :: Sing r) ->
-    (~>:~:) @x @a @b @r @(WhyCongSym x y f a) singEq Refl
+    (~>:~:) @x @a @b @(WhyCongSym x y f a) @r singEq Refl
+
+type WhyEqIsRefl (a :: k) (z :: k) (e :: a :~: z)
+  = e :~~: (Refl :: a :~: a)
+data WhyEqIsReflSym (a :: k) :: forall (z :: k). a :~: z ~> Type
+type instance Apply (WhyEqIsReflSym a :: a :~: z ~> Type) e = WhyEqIsRefl a z e
+
+eqIsRefl :: forall (k :: Type) (a :: k) (b :: k) (e :: a :~: b).
+            Sing e -> e :~~: (Refl :: a :~: a)
+eqIsRefl eq = (~>:~:) @k @a @b @(WhyEqIsReflSym a) @e eq HRefl
+
+type WhyHEqIsHRefl (a :: j) (z :: k) (e :: a :~~: z)
+  = e :~~: (HRefl :: a :~~: a)
+data WhyHEqIsHReflSym (a :: j) :: forall (k :: Type) (z :: k). a :~~: z ~> Type
+type instance Apply (WhyHEqIsHReflSym a :: a :~~: z ~> Type) e = WhyHEqIsHRefl a z e
+
+heqIsHRefl :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (e :: a :~~: b).
+              Sing e -> e :~~: (HRefl :: a :~~: a)
+heqIsHRefl heq = (~>:~~:) @j @k @a @b @(WhyHEqIsHReflSym a) @e heq HRefl
diff --git a/tests/PeanoSpec.hs b/tests/PeanoSpec.hs
deleted file mode 100644
--- a/tests/PeanoSpec.hs
+++ /dev/null
@@ -1,117 +0,0 @@
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeInType #-}
-{-# LANGUAGE TypeOperators #-}
-module PeanoSpec where
-
-import Data.Kind
-import Data.Singletons
-
-import PeanoTypes
-
-import Test.Hspec
-
-main :: IO ()
-main = hspec spec
-
-spec :: Spec
-spec = parallel $ do
-  describe "replicateVec" $ do
-    it "works with empty lists" $
-      replicateVec SZ () `shouldBe` VNil
-    it "works with non-empty lists" $
-      replicateVec (SS SZ) () `shouldBe` () :# VNil
-  describe "mapVec" $ do
-    it "maps over a Vec" $ do
-      mapVec reverse ("hello" :# "world" :# VNil)
-          `shouldBe` ("olleh" :# "dlrow" :# VNil)
-  describe "zipWithVec" $ do
-    it "zips two Vecs" $ do
-      zipWithVec (,) ((2 :: Int) :# 22 :# VNil)
-                     ("chicken-of-the-woods" :# "hen-of-woods" :# VNil)
-        `shouldBe` ((2, "chicken-of-the-woods") :# (22, "hen-of-woods")
-                                                :# VNil)
-  describe "appendVec" $ do
-    it "appends two Vecs" $ do
-      appendVec ("portabello" :# "bay-bolete"
-                              :# "funnel-chantrelle"
-                              :# VNil)
-                ("sheathed-woodtuft" :# "puffball" :# VNil)
-        `shouldBe` ("portabello" :# "bay-bolete"
-                                 :# "funnel-chantrelle"
-                                 :# "sheathed-woodtuft"
-                                 :# "puffball"
-                                 :# VNil)
-  describe "transposeVec" $ do
-    it "transposes a Vec" $ do
-      transposeVec (('a' :# 'b' :# 'c' :# VNil)
-                 :# ('d' :# 'e' :# 'f' :# VNil)
-                 :# VNil)
-        `shouldBe`
-                   (('a' :# 'd' :# VNil)
-                 :# ('b' :# 'e' :# VNil)
-                 :# ('c' :# 'f' :# VNil)
-                 :# VNil)
-
------
-
-replicateVec :: forall (e :: Type) (howMany :: Peano).
-                Sing howMany -> e -> Vec e howMany
-replicateVec s e = elimPeano @(TyCon1 (Vec e)) @howMany s VNil step
-  where
-    step :: forall (k :: Peano). Sing k -> Vec e k -> Vec e (S k)
-    step _ = (e :#)
-
-mapVec :: forall (a :: Type) (b :: Type) (n :: Peano).
-          SingI n
-       => (a -> b) -> Vec a n -> Vec b n
-mapVec f = elimPeano @(WhyMapVecSym2 a b) @n (sing @_ @n) base step
-  where
-    base :: WhyMapVec a b Z
-    base _ = VNil
-
-    step :: forall (k :: Peano). Sing k -> WhyMapVec a b k -> WhyMapVec a b (S k)
-    step _ mapK vK = f (vhead vK) :# mapK (vtail vK)
-
-zipWithVec :: forall (a :: Type) (b :: Type) (c :: Type) (n :: Peano).
-              SingI n
-           => (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n
-zipWithVec f = elimPeano @(WhyZipWithVecSym3 a b c) @n (sing @_ @n) base step
-  where
-    base :: WhyZipWithVec a b c Z
-    base _ _ = VNil
-
-    step :: forall (k :: Peano).
-            Sing k
-         -> WhyZipWithVec a b c k
-         -> WhyZipWithVec a b c (S k)
-    step _ zwK vaK vbK = f   (vhead vaK) (vhead vbK)
-                      :# zwK (vtail vaK) (vtail vbK)
-
-appendVec :: forall (e :: Type) (n :: Peano) (m :: Peano).
-             SingI n
-          => Vec e n -> Vec e m -> Vec e (n `Plus` m)
-appendVec = elimPeano @(WhyAppendVecSym2 e m) @n (sing @_ @n) base step
-  where
-    base :: WhyAppendVec e m Z
-    base _ = id
-
-    step :: forall (k :: Peano).
-            Sing k
-         -> WhyAppendVec e m k
-         -> WhyAppendVec e m (S k)
-    step _ avK vK1 vK2 = vhead vK1 :# avK (vtail vK1) vK2
-
-transposeVec :: forall (e :: Type) (n :: Peano) (m :: Peano).
-                (SingI n, SingI m)
-             => Vec (Vec e m) n -> Vec (Vec e n) m
-transposeVec = elimPeano @(WhyTransposeVecSym2 e m) @n (sing @_ @n) base step
-  where
-    base :: WhyTransposeVec e m Z
-    base _ = replicateVec (sing @_ @m) VNil
-
-    step :: forall (k :: Peano).
-            Sing k
-         -> WhyTransposeVec e m k
-         -> WhyTransposeVec e m (S k)
-    step _ transK vK = zipWithVec (:#) (vhead vK) (transK (vtail vK))
diff --git a/tests/PeanoTypes.hs b/tests/PeanoTypes.hs
deleted file mode 100644
--- a/tests/PeanoTypes.hs
+++ /dev/null
@@ -1,94 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-module PeanoTypes where
-
-import Data.Eliminator.TH
-import Data.Kind
-import Data.Singletons.TH
-
-$(singletons [d|
-  data Peano = Z | S Peano
-
-  infixl 6 `plus`
-  plus :: Peano -> Peano -> Peano
-  plus Z     m = m
-  plus (S k) m = S (plus k m)
-
-  infixl 7 `times`
-  times :: Peano -> Peano -> Peano
-  times Z     _ = Z
-  times (S k) m = plus m (times k m)
-  |])
-$(deriveElim ''Peano)
-
-data Vec a (n :: Peano) where
-  VNil :: Vec a Z
-  (:#) :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n)
-infixr 5 :#
-deriving instance Eq a   => Eq (Vec a n)
-deriving instance Ord a  => Ord (Vec a n)
-deriving instance Show a => Show (Vec a n)
-
-data instance Sing (z :: Vec a n) where
-  SVNil :: Sing VNil
-  (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (x :# xs)
-type SVec = (Sing :: Vec a n -> Type)
-infixr 5 :%#
-
-instance SingKind a => SingKind (Vec a n) where
-  type Demote (Vec a n) = Vec (Demote a) n
-  fromSing SVNil      = VNil
-  fromSing (x :%# xs) = fromSing x :# fromSing xs
-  toSing VNil = SomeSing SVNil
-  toSing (x :# xs) =
-    withSomeSing x $ \sx ->
-      withSomeSing xs $ \sxs ->
-        SomeSing $ sx :%# sxs
-
-instance SingI VNil where
-  sing = SVNil
-
-instance (SingI x, SingI xs) => SingI (x :# xs) where
-  sing = sing :%# sing
-
-elimVec :: forall (a :: Type) (n :: Peano)
-                  (p :: forall (k :: Peano). Vec a k ~> Type) (v :: Vec a n).
-           Sing v
-        -> p @@ VNil
-        -> (forall (k :: Peano) (x :: a) (xs :: Vec a k).
-                   Sing x -> Sing xs -> p @@ xs -> p @@ (x :# xs))
-        -> p @@ v
-elimVec SVNil pVNil _ = pVNil
-elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =
-  pVCons sx sxs (elimVec @a @k @p @xs sxs pVNil pVCons)
-
-type WhyMapVec (a :: Type) (b :: Type) (n :: Peano) = Vec a n -> Vec b n
-$(genDefunSymbols [''WhyMapVec])
-
-type WhyZipWithVec (a :: Type) (b :: Type) (c :: Type) (n :: Peano)
-  = Vec a n -> Vec b n -> Vec c n
-$(genDefunSymbols [''WhyZipWithVec])
-
-type WhyAppendVec (e :: Type) (m :: Peano) (n :: Peano)
-  = Vec e n -> Vec e m -> Vec e (n `Plus` m)
-$(genDefunSymbols [''WhyAppendVec])
-
-type WhyTransposeVec (e :: Type) (m :: Peano) (n :: Peano)
-  = Vec (Vec e m) n -> Vec (Vec e n) m
-$(genDefunSymbols [''WhyTransposeVec])
-
-type WhyConcatVec (e :: Type) (j :: Peano) (n :: Peano) (l :: Vec (Vec e j) n)
-  = Vec e (n `Times` j)
-data WhyConcatVecSym (e :: Type) (j :: Peano)
-  :: forall (n :: Peano). Vec (Vec e j) n ~> Type
-type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l
-  = WhyConcatVec e j n l
diff --git a/tests/VecSpec.hs b/tests/VecSpec.hs
--- a/tests/VecSpec.hs
+++ b/tests/VecSpec.hs
@@ -5,11 +5,13 @@
 {-# LANGUAGE TypeOperators #-}
 module VecSpec where
 
+import Data.Eliminator
 import Data.Kind
+import Data.Nat
 import Data.Singletons
+import Data.Singletons.Prelude.Num
 
-import PeanoSpec (appendVec)
-import PeanoTypes
+import VecTypes
 
 import Test.Hspec
 
@@ -18,6 +20,43 @@
 
 spec :: Spec
 spec = parallel $ do
+  describe "replicateVec" $ do
+    it "works with empty lists" $
+      replicateVec (sLit @0) () `shouldBe` VNil
+    it "works with non-empty lists" $ do
+      replicateVec (sLit @1) () `shouldBe` () :# VNil
+      replicateVec (sLit @2) () `shouldBe` () :# () :# VNil
+  describe "mapVec" $ do
+    it "maps over a Vec" $ do
+      mapVec reverse ("hello" :# "world" :# VNil)
+          `shouldBe` ("olleh" :# "dlrow" :# VNil)
+  describe "zipWithVec" $ do
+    it "zips two Vecs" $ do
+      zipWithVec (,) ((2 :: Int) :# 22 :# VNil)
+                     ("chicken-of-the-woods" :# "hen-of-woods" :# VNil)
+        `shouldBe` ((2, "chicken-of-the-woods") :# (22, "hen-of-woods")
+                                                :# VNil)
+  describe "appendVec" $ do
+    it "appends two Vecs" $ do
+      appendVec ("portabello" :# "bay-bolete"
+                              :# "funnel-chantrelle"
+                              :# VNil)
+                ("sheathed-woodtuft" :# "puffball" :# VNil)
+        `shouldBe` ("portabello" :# "bay-bolete"
+                                 :# "funnel-chantrelle"
+                                 :# "sheathed-woodtuft"
+                                 :# "puffball"
+                                 :# VNil)
+  describe "transposeVec" $ do
+    it "transposes a Vec" $ do
+      transposeVec (('a' :# 'b' :# 'c' :# VNil)
+                 :# ('d' :# 'e' :# 'f' :# VNil)
+                 :# VNil)
+        `shouldBe`
+                   (('a' :# 'd' :# VNil)
+                 :# ('b' :# 'e' :# VNil)
+                 :# ('c' :# 'f' :# VNil)
+                 :# VNil)
   describe "concatVec" $ do
     it "concats a Vec of Vecs" $ do
       concatVec ((False :# True  :# False :# VNil)
@@ -28,16 +67,77 @@
 
 -----
 
-concatVec :: forall (e :: Type) (n :: Peano) (j :: Peano).
+replicateVec :: forall (e :: Type) (howMany :: Nat).
+                Sing howMany -> e -> Vec e howMany
+replicateVec s e = elimNat @(TyCon1 (Vec e)) @howMany s VNil step
+  where
+    step :: forall (k :: Nat). Sing k -> Vec e k -> Vec e (S k)
+    step _ = (e :#)
+
+mapVec :: forall (a :: Type) (b :: Type) (n :: Nat).
+          SingI n
+       => (a -> b) -> Vec a n -> Vec b n
+mapVec f = elimNat @(WhyMapVecSym2 a b) @n (sing @_ @n) base step
+  where
+    base :: WhyMapVec a b Z
+    base _ = VNil
+
+    step :: forall (k :: Nat). Sing k -> WhyMapVec a b k -> WhyMapVec a b (S k)
+    step _ mapK vK = f (vhead vK) :# mapK (vtail vK)
+
+zipWithVec :: forall (a :: Type) (b :: Type) (c :: Type) (n :: Nat).
+              SingI n
+           => (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n
+zipWithVec f = elimNat @(WhyZipWithVecSym3 a b c) @n (sing @_ @n) base step
+  where
+    base :: WhyZipWithVec a b c Z
+    base _ _ = VNil
+
+    step :: forall (k :: Nat).
+            Sing k
+         -> WhyZipWithVec a b c k
+         -> WhyZipWithVec a b c (S k)
+    step _ zwK vaK vbK = f   (vhead vaK) (vhead vbK)
+                      :# zwK (vtail vaK) (vtail vbK)
+
+appendVec :: forall (e :: Type) (n :: Nat) (m :: Nat).
+             SingI n
+          => Vec e n -> Vec e m -> Vec e (n :+ m)
+appendVec = elimNat @(WhyAppendVecSym2 e m) @n (sing @_ @n) base step
+  where
+    base :: WhyAppendVec e m Z
+    base _ = id
+
+    step :: forall (k :: Nat).
+            Sing k
+         -> WhyAppendVec e m k
+         -> WhyAppendVec e m (S k)
+    step _ avK vK1 vK2 = vhead vK1 :# avK (vtail vK1) vK2
+
+transposeVec :: forall (e :: Type) (n :: Nat) (m :: Nat).
+                (SingI n, SingI m)
+             => Vec (Vec e m) n -> Vec (Vec e n) m
+transposeVec = elimNat @(WhyTransposeVecSym2 e m) @n (sing @_ @n) base step
+  where
+    base :: WhyTransposeVec e m Z
+    base _ = replicateVec (sing @_ @m) VNil
+
+    step :: forall (k :: Nat).
+            Sing k
+         -> WhyTransposeVec e m k
+         -> WhyTransposeVec e m (S k)
+    step _ transK vK = zipWithVec (:#) (vhead vK) (transK (vtail vK))
+
+concatVec :: forall (e :: Type) (n :: Nat) (j :: Nat).
              (SingKind e, SingI j, e ~ Demote e)
-          => Vec (Vec e j) n -> Vec e (n `Times` j)
+          => Vec (Vec e j) n -> Vec e (n :* j)
 concatVec l = withSomeSing l $ \(singL :: Sing l) ->
                 elimVec @(Vec e j) @n @(WhyConcatVecSym e j) @l singL base step
   where
     base :: WhyConcatVec e j Z VNil
     base = VNil
 
-    step :: forall (k :: Peano) (x :: Vec e j) (xs :: Vec (Vec e j) k).
+    step :: forall (k :: Nat) (x :: Vec e j) (xs :: Vec (Vec e j) k).
                    Sing x -> Sing xs
                 -> WhyConcatVec e j k     xs
                 -> WhyConcatVec e j (S k) (x :# xs)
diff --git a/tests/VecTypes.hs b/tests/VecTypes.hs
new file mode 100644
--- /dev/null
+++ b/tests/VecTypes.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module VecTypes where
+
+import Data.Kind
+import Data.Nat
+import Data.Singletons.Prelude.Num
+import Data.Singletons.TH
+
+data Vec :: Type -> Nat -> Type where
+  VNil :: Vec a Z
+  (:#) :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n)
+infixr 5 :#
+deriving instance Eq a   => Eq (Vec a n)
+deriving instance Ord a  => Ord (Vec a n)
+deriving instance Show a => Show (Vec a n)
+
+data instance Sing (z :: Vec a n) where
+  SVNil :: Sing VNil
+  (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (x :# xs)
+type SVec = (Sing :: Vec a n -> Type)
+infixr 5 :%#
+
+instance SingKind a => SingKind (Vec a n) where
+  type Demote (Vec a n) = Vec (Demote a) n
+  fromSing SVNil      = VNil
+  fromSing (x :%# xs) = fromSing x :# fromSing xs
+  toSing VNil = SomeSing SVNil
+  toSing (x :# xs) =
+    withSomeSing x $ \sx ->
+      withSomeSing xs $ \sxs ->
+        SomeSing $ sx :%# sxs
+
+instance SingI VNil where
+  sing = SVNil
+
+instance (SingI x, SingI xs) => SingI (x :# xs) where
+  sing = sing :%# sing
+
+elimVec :: forall (a :: Type) (n :: Nat)
+                  (p :: forall (k :: Nat). Vec a k ~> Type) (v :: Vec a n).
+           Sing v
+        -> p @@ VNil
+        -> (forall (k :: Nat) (x :: a) (xs :: Vec a k).
+                   Sing x -> Sing xs -> p @@ xs -> p @@ (x :# xs))
+        -> p @@ v
+elimVec SVNil pVNil _ = pVNil
+elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =
+  pVCons sx sxs (elimVec @a @k @p @xs sxs pVNil pVCons)
+
+type WhyMapVec (a :: Type) (b :: Type) (n :: Nat) = Vec a n -> Vec b n
+$(genDefunSymbols [''WhyMapVec])
+
+type WhyZipWithVec (a :: Type) (b :: Type) (c :: Type) (n :: Nat)
+  = Vec a n -> Vec b n -> Vec c n
+$(genDefunSymbols [''WhyZipWithVec])
+
+type WhyAppendVec (e :: Type) (m :: Nat) (n :: Nat)
+  = Vec e n -> Vec e m -> Vec e (n :+ m)
+$(genDefunSymbols [''WhyAppendVec])
+
+type WhyTransposeVec (e :: Type) (m :: Nat) (n :: Nat)
+  = Vec (Vec e m) n -> Vec (Vec e n) m
+$(genDefunSymbols [''WhyTransposeVec])
+
+type WhyConcatVec (e :: Type) (j :: Nat) (n :: Nat) (l :: Vec (Vec e j) n)
+  = Vec e (n :* j)
+data WhyConcatVecSym (e :: Type) (j :: Nat)
+  :: forall (n :: Nat). Vec (Vec e j) n ~> Type
+type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l
+  = WhyConcatVec e j n l