diff --git a/src/TypeUnary/Nat.hs b/src/TypeUnary/Nat.hs
--- a/src/TypeUnary/Nat.hs
+++ b/src/TypeUnary/Nat.hs
@@ -1,6 +1,10 @@
 {-# LANGUAGE TypeOperators, GADTs, KindSignatures, RankNTypes #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+
+-- Experiment
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, CPP #-}
+
 {-# OPTIONS_GHC -Wall #-}
 ----------------------------------------------------------------------
 -- |
@@ -18,11 +22,12 @@
   (
     module TypeUnary.TyNat
   -- * Value-typed natural numbers
-  , Nat(..), zero, one, two, three, four
+  , Nat(..), predN, zero, one, two, three, four
   , withIsNat, natSucc, natIsNat
   , natToZ, natEq, natAdd, natMul
   , IsNat(..)
   , induction
+  , PlusZero, plusZero
   -- * Inequality proofs and indices
   , (:<:)(..), succLim
   , Index(..), unIndex, succI, index0, index1, index2, index3
@@ -37,6 +42,8 @@
 import Data.Maybe (isJust)
 import Data.Typeable (Typeable)
 
+import Data.Constraint (Dict(..))
+
 import Data.Proof.EQ
 
 import TypeUnary.TyNat
@@ -61,6 +68,9 @@
 natIsNat Zero     = Zero
 natIsNat (Succ n) = Succ n
 
+predN :: Nat (S n) -> Nat n
+predN (Succ n) = n
+
 {-
 
 -- Another approach (also works):
@@ -118,17 +128,28 @@
 -- from IsNat.
 
 -- | Peano's induction principle
-induction :: forall p. 
-             p Z -> (forall n. IsNat n => p n -> p (S n))
-          -> (forall n. IsNat n => p n)
-induction z s = go nat
+induction :: forall p . 
+             p Z => (forall n. IsNat n => Dict (p n) -> Dict (p (S n)))
+          -> (forall n. IsNat n => Dict (p n))
+induction s = go nat
  where
-   -- morphism over z & s.
-   go :: forall n. Nat n -> p n
-   go Zero     = z
+   go :: forall n. Nat n -> Dict (p n)
+   go Zero     = Dict
    go (Succ m) = s (go m)
 
--- TODO: Use induction for n + Z == n. Then associativity and commutativity.
+class    (n :+: Z) ~ n => PlusZero n
+instance (n :+: Z) ~ n => PlusZero n
+
+plusZero :: IsNat n => Dict (PlusZero n)
+plusZero = induction (\ Dict -> Dict)
+
+#if 0
+class    ((p :+: q) :+: r) ~ (p :+: (q :+: r)) => PlusAssocR p q r
+instance ((p :+: q) :+: r) ~ (p :+: (q :+: r)) => PlusAssocR p q r
+
+plusAssocR :: (IsNat p, IsNat q, IsNat r) => Dict (PlusAssocR p q r)
+plusAssocR ...
+#endif
 
 {--------------------------------------------------------------------
     Inequality proofs
diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs
--- a/src/TypeUnary/Vec.hs
+++ b/src/TypeUnary/Vec.hs
@@ -45,7 +45,7 @@
 
 import Prelude hiding (foldr,sum,and)
 
-import Data.Monoid (Monoid(..))
+import Data.Monoid (Monoid(..),(<>))
 import Control.Applicative (Applicative(..),liftA2,(<$>))
 import Data.Foldable (Foldable(..),toList,sum) -- ,and
 import Data.Traversable (Traversable(..))
@@ -56,6 +56,8 @@
 
 import Control.Newtype (Newtype(..))
 
+-- import Data.Constraint
+
 import Data.VectorSpace
 
 import TypeUnary.Nat
@@ -176,25 +178,41 @@
   {-# INLINE fmap #-}
 
 instance IsNat n => Applicative (Vec n) where
-  pure  = pureV
-  (<*>) = applyV
+  pure  = pureV nat
+  (<*>) = applyV nat
+  {-# INLINE pure  #-}
+  {-# INLINE (<*>) #-}
 
-pureV :: IsNat n => a -> Vec n a
-pureV = pureV' nat
+pureV :: Nat n -> a -> Vec n a
+pureV Zero     _ = ZVec
+pureV (Succ n) a = a :< pureV n a
+{-# INLINE pureV #-}
 
-pureV' :: Nat n -> a -> Vec n a
-pureV' Zero     _ = ZVec
-pureV' (Succ n) a = a :< pureV' n a
+-- Experiment
 
-applyV :: Vec n (a -> b) -> Vec n a -> Vec n b
-ZVec      `applyV` ZVec      = ZVec
-(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)
-_ `applyV` _ = cant "applyV"
+inVecS :: ((a, Vec n a) -> (b, Vec n b)) -> (Vec (S n) a -> Vec (S n) b)
+inVecS f = uncurry (:<) . f . unConsV
 
--- Without -fno-warn-incomplete-patterns above,
--- the previous two instances lead to warnings about non-exhaustive
--- pattern matches, although the other possibilities
--- are type-incorrect.  According to SLPJ:
+inVecS2 :: ((a, Vec n a) -> (b, Vec n b) -> (c, Vec n c))
+        -> (Vec (S n) a  -> Vec (S n) b  -> Vec (S n) c )
+inVecS2 f = inVecS . f . unConsV
+
+-- TODO: reconcile unConsV vs unVecS
+
+applyV :: Nat n -> Vec n (a -> b) -> Vec n a -> Vec n b
+applyV Zero     = \ _      _      -> ZVec
+applyV (Succ n) = inVecS2 (\ (f,fs) (x,xs) -> (f x , applyV n fs xs))
+{-# INLINE applyV #-}
+
+-- applyV :: Nat n -> Vec n (a -> b) -> Vec n a -> Vec n b
+-- applyV Zero     = \ ZVec      ZVec      -> ZVec
+-- applyV (Succ n) = \ (f :< fs) (x :< xs) -> f x :< applyV n fs xs
+-- {-# INLINE applyV #-}
+
+-- The "= \ ..." form here side-steps the incomplete patterns warning without
+-- -fno-warn-incomplete-patterns above. Otherwise we get warnings about
+-- non-exhaustive pattern matches, although the other possibilities are
+-- type-incorrect. Once upon a time SLPJ said
 -- 
 --   The overlap warning checker simply doesn't take account of GADTs.
 --   There's a long-standing project suggestion to fix this:
@@ -212,9 +230,9 @@
 joinV _ = cant "joinV"
 
 instance Foldable (Vec n) where
-  foldr _  b ZVec     = b
-  foldr h b (a :< as) = a `h` foldr h b as
-  {-# INLINE foldr #-}
+  foldMap _ ZVec      = mempty
+  foldMap h (a :< as) = h a <> foldMap h as
+  {-# INLINE foldMap #-}
 
 instance Traversable (Vec n) where
   traverse _ ZVec      = pure ZVec
@@ -539,16 +557,42 @@
 -- 
 -- Won't type-check without commutativity of addition. :(
 
-{-
+#if 0
 
+addZ :: IsNat n => Dict (n ~ (n :+: Z))
+addZ = addZ' nat
+
+addZ' :: Nat n -> Dict (n ~ (n :+: Z))
+addZ' Zero                       = Dict
+addZ' (Succ m) | Dict <- addZ' m = Dict
+
+add1 :: IsNat m => Dict ((m :+: S Z) ~ S m)
+add1 = add1' nat
+
+add1' :: Nat m -> Dict ((m :+: S Z) ~ S m)
+add1' Zero                       = Dict
+add1' (Succ m) | Dict <- add1' m = Dict
+
+-- addS :: (IsNat m, IsNat n) => Dict ((m :+: S n) ~ S (m :+: n))
+-- addS = addS' nat
+
+addS' :: IsNat m => Nat n -> Dict ((m :+: S n) ~ S (m :+: n))
+addS' Zero | Dict <- add1 = Dict
+...
+
+-- Oops: non-injectivity
+
 -- Reversal. Thinking about this one. Currently thwarted by missing
 -- knowledge about numbers in the type-checker. Would be easy with
 -- built-in type-level naturals.
 
 -- | Reverse a vector
-reverseV :: Vec n a -> Vec n a
-reverseV = reverse' nat ZVec
+reverseV :: forall n a. IsNat n => Vec n a -> Vec n a
+reverseV | Dict <- (addZ :: Dict (n ~ (n :+: Z))) = reverse' nat ZVec
 
+-- reverseV :: Vec n a -> Vec n a
+-- reverseV = reverse' nat ZVec
+
 --  Couldn't match type `n' with `n :+: Z'
 
 -- Reverse na and append to ma
@@ -557,7 +601,7 @@
 reverse' (Succ n) ma (a :< as) = reverse' n (a :< ma) as
 
 -- Could not deduce ((n1 :+: S m) ~ S (n1 :+: m))
--}
+#endif
 
 -- | Delete exactly one occurrence of an element from a vector, raising an
 -- error if the element isn't present.
@@ -646,11 +690,13 @@
 
 instance IsNat n => ToVec [a] n a where
   toVec = toVecL nat
+  {-# INLINE toVec #-}
 
 toVecL :: Nat n -> [a] -> Vec n a
 toVecL Zero [] = ZVec
 toVecL (Succ m) (a:as) = a :< toVecL m as
 toVecL _ _ = error "toVecL: length mismatch"
+{-# INLINE toVecL #-}
 
 {--------------------------------------------------------------------
     Misc
diff --git a/type-unary.cabal b/type-unary.cabal
--- a/type-unary.cabal
+++ b/type-unary.cabal
@@ -1,5 +1,5 @@
 Name:                type-unary
-Version:             0.2.16
+Version:             0.2.19
 Cabal-Version:       >= 1.6
 Synopsis:            
   Type-level and typed unary natural numbers, inequality proofs, vectors
@@ -26,6 +26,7 @@
   hs-Source-Dirs:      src
   Extensions:
   Build-Depends:       base >=4 && < 5
+                     , constraints
                      , newtype >= 0.2
                      , ty >= 0.1.5
                      , vector-space