diff --git a/CHANGES b/CHANGES
deleted file mode 100644
--- a/CHANGES
+++ /dev/null
@@ -1,19 +0,0 @@
-1.0:
-
-* Change representation of decimals to an inherently normalized form
-  that is symmetric with respect to positive and negative numbers.
-
-* singularize module names
-
-* separate Decimal and general representation
-
-* use Proxys instead of plain types for data functions
-  This is also consistent with new Nat kind,
-  where types of kind Nat have no data values.
-
-* Ord: make infix operators classes and prefix functions type functions
-  It seems to be more natural to me to write
-     x :<: y   and   GTT x y ~ True
-
-* Num, Bool, Ord: remove T suffixes from functions
-  Use qualification instead.
diff --git a/Changes.md b/Changes.md
new file mode 100644
--- /dev/null
+++ b/Changes.md
@@ -0,0 +1,19 @@
+1.0:
+
+* Change representation of decimals to an inherently normalized form
+  that is symmetric with respect to positive and negative numbers.
+
+* singularize module names
+
+* separate Decimal and general representation
+
+* use Proxys instead of plain types for data functions
+  This is also consistent with new Nat kind,
+  where types of kind Nat have no data values.
+
+* Ord: make infix operators classes and prefix functions type functions
+  It seems to be more natural to me to write
+     x :<: y   and   GTT x y ~ True
+
+* Num, Bool, Ord: remove T suffixes from functions
+  Use qualification instead.
diff --git a/src/Type/Base/Proxy.hs b/src/Type/Base/Proxy.hs
--- a/src/Type/Base/Proxy.hs
+++ b/src/Type/Base/Proxy.hs
@@ -2,7 +2,12 @@
 
 import Control.Applicative (Applicative, pure, (<*>), )
 
+import qualified Prelude as P
+import Prelude (String, Eq, Functor, fmap)
+
+
 data Proxy a = Proxy
+   deriving (Eq)
 
 instance Functor Proxy where
    fmap _f Proxy = Proxy
@@ -10,3 +15,10 @@
 instance Applicative Proxy where
    pure _ = Proxy
    Proxy <*> Proxy = Proxy
+
+
+class Show a where
+   showsPrec :: P.Int -> Proxy a -> P.ShowS
+
+instance Show a => P.Show (Proxy a) where
+   showsPrec = showsPrec
diff --git a/src/Type/Data/Num.hs b/src/Type/Data/Num.hs
--- a/src/Type/Data/Num.hs
+++ b/src/Type/Data/Num.hs
@@ -55,6 +55,10 @@
     , Natural
     , Positive
     , Negative
+    , integerFromSingleton
+    , integralFromSingleton
+    , singletonFromProxy
+    , integralFromProxy
     , fromInteger
     , reifyPositive
     , reifyNegative
@@ -184,10 +188,21 @@
 newtype Singleton d = Singleton P.Integer
 
 
-fromInteger :: forall x y. (Integer x, Num y) => Proxy x -> y
-fromInteger _ =
-    case singleton :: Singleton x of
-        Singleton n -> P.fromInteger n
+integerFromSingleton :: (Integer x) => Singleton x -> P.Integer
+integerFromSingleton (Singleton n) = n
+
+integralFromSingleton :: (Integer x, Num y) => Singleton x -> y
+integralFromSingleton = P.fromInteger . integerFromSingleton
+
+singletonFromProxy :: (Integer x) => Proxy x -> Singleton x
+singletonFromProxy Proxy = singleton
+
+integralFromProxy :: (Integer x, Num y) => Proxy x -> y
+integralFromProxy = integralFromSingleton . singletonFromProxy
+
+-- | synonym for 'integralFromProxy', kept for backward compatibility
+fromInteger :: (Integer x, Num y) => Proxy x -> y
+fromInteger = integralFromProxy
 
 
 --- positive and negative assertions: unsafe, in a trusted kernel
diff --git a/src/Type/Data/Num/Decimal/Number.hs b/src/Type/Data/Num/Decimal/Number.hs
--- a/src/Type/Data/Num/Decimal/Number.hs
+++ b/src/Type/Data/Num/Decimal/Number.hs
@@ -35,6 +35,7 @@
 import qualified Type.Data.Num.Unary as Unary
 import qualified Type.Data.Num as Op
 import qualified Type.Data.Ord as Ord
+import qualified Type.Base.Proxy as Proxy
 
 import Type.Data.Num.Decimal.Digit
           (Dec0, Dec1, Dec2, Dec3, Dec4, Dec5, Dec6, Dec7, Dec8, Dec9)
@@ -46,6 +47,8 @@
 import Data.Tuple.HT (swap)
 import qualified Data.List as List
 
+import Text.Printf (printf)
+
 import qualified Prelude as P
 import Prelude hiding (Integer)
 
@@ -97,6 +100,16 @@
 
 decimal :: Proxy n -> Proxy (Dec n)
 decimal Proxy = Proxy
+
+stripDec :: Proxy (Dec n) -> Proxy n
+stripDec Proxy = Proxy
+
+
+instance Integer a => Proxy.Show (Dec a) where
+   showsPrec prec =
+      (\n -> showParen (prec>10) (showString (printf "decimal d%d" n)))
+       . integerFromSingleton . singletonFromProxy . stripDec
+
 
 reifyIntegral :: P.Integer -> (forall s. Integer s => Proxy s -> w) -> w
 reifyIntegral n f =
diff --git a/src/Type/Data/Num/Unary.hs b/src/Type/Data/Num/Unary.hs
--- a/src/Type/Data/Num/Unary.hs
+++ b/src/Type/Data/Num/Unary.hs
@@ -3,16 +3,21 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Type.Data.Num.Unary (
-    Unary, Un, Zero, Succ, zero, succ,
+    Unary, unary, Un, Zero, Succ, zero, succ,
     Singleton(..), singleton, singletonFromProxy,
     integerFromSingleton, integralFromSingleton,
+    integralFromProxy,
     Natural(..), Positive(..),
     (:+:), (:*:),
+    reifyNatural,
     ) where
 
 import qualified Type.Data.Num as Num
+import qualified Type.Base.Proxy as Proxy
 import Type.Base.Proxy (Proxy(Proxy))
 
+import Text.Printf (printf)
+
 import Prelude hiding (succ)
 
 
@@ -96,13 +101,19 @@
 singletonFromProxy :: (Natural n) => Proxy n -> Singleton n
 singletonFromProxy Proxy = singleton
 
+integralFromProxy :: (Natural n, Num a) => Proxy n -> a
+integralFromProxy = integralFromSingleton . singletonFromProxy
 
+
 instance Num.Representation Unary where
     reifyIntegral _ i k = reifyIntegral i (k . unary)
 
 unary :: Proxy n -> Proxy (Un n)
 unary Proxy = Proxy
 
+stripUn :: Proxy (Un n) -> Proxy n
+stripUn Proxy = Proxy
+
 reifyIntegral :: Integer -> (forall s. Natural s => Proxy s -> w) -> w
 reifyIntegral n f =
     if n < 0
@@ -118,3 +129,9 @@
 
 type instance Un x Num.:+: Un y = Un (x :+: y)
 type instance Un x Num.:*: Un y = Un (x :*: y)
+
+
+instance Natural a => Proxy.Show (Un a) where
+   showsPrec prec =
+      (\n -> showParen (prec>10) (showString (printf "unary u%d" n)))
+       . integerFromSingleton . singletonFromProxy . stripUn
diff --git a/src/Type/Data/Num/Unary/Proof.hs b/src/Type/Data/Num/Unary/Proof.hs
--- a/src/Type/Data/Num/Unary/Proof.hs
+++ b/src/Type/Data/Num/Unary/Proof.hs
@@ -1,15 +1,19 @@
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE FlexibleContexts #-}
 module Type.Data.Num.Unary.Proof (
     Nat(..), Pos(..),
     natFromPos,
     addNat, addPosL, addPosR,
+    AddZeroL(..), addZeroL,
+    AddComm(..), addComm,
+    AddAssoc(..), addAssoc,
     mulNat, mulPos,
     ) where
 
 import Type.Data.Num.Unary
-          (Natural, Positive, Succ, switchNat, switchPos, (:+:), (:*:))
+          (Natural, Positive, Zero, Succ, switchNat, switchPos, (:+:), (:*:))
 
 data Nat x = Natural x => Nat
 data Pos x = Positive x => Pos
@@ -33,76 +37,131 @@
 
 
 newtype
-   AddNatTheorem x y =
-      AddNatTheorem {
-         runAddNatTheorem :: Nat x -> Nat y -> Nat (x :+: y)
-      }
+   QuantifiedAdd condx condy prop x y =
+      QuantifiedAdd {runQuantifiedAdd :: condx x -> condy y -> prop (x :+: y)}
 
 addNat :: Nat x -> Nat y -> Nat (x :+: y)
 addNat x0 y0@Nat =
-   runAddNatTheorem
+   runQuantifiedAdd
       (switchNat
-         (AddNatTheorem $ \Nat Nat -> Nat)
-         (AddNatTheorem $ \x -> succNat . addNat x . prevNat))
+         (QuantifiedAdd const)
+         (QuantifiedAdd $ \x -> succNat . addNat x . prevNat))
       x0 y0
 
-
-newtype
-   AddPosRTheorem x y =
-      AddPosRTheorem {
-         runAddPosRTheorem :: Nat x -> Pos y -> Pos (x :+: y)
-      }
-
 addPosR :: Nat x -> Pos y -> Pos (x :+: y)
 addPosR x0 y0@Pos =
-   runAddPosRTheorem
-      (switchPos
-         (AddPosRTheorem $ \x ->
-             posSucc . addNat x . prevPos))
+   runQuantifiedAdd
+      (switchPos (QuantifiedAdd $ \x -> posSucc . addNat x . prevPos))
       x0 y0
 
-
-newtype
-   AddPosLTheorem x y =
-      AddPosLTheorem {
-         runAddPosLTheorem :: Pos x -> Nat y -> Pos (x :+: y)
-      }
-
 addPosL :: Pos x -> Nat y -> Pos (x :+: y)
 addPosL x0 y0@Nat =
-   runAddPosLTheorem
+   runQuantifiedAdd
       (switchNat
-         (AddPosLTheorem $ \x _y -> x)
-         (AddPosLTheorem $ \x ->
-            posSucc . addNat (natFromPos x) . prevNat))
+         (QuantifiedAdd const)
+         (QuantifiedAdd $ \x -> posSucc . addNat (natFromPos x) . prevNat))
       x0 y0
 
 
+newtype Quantified prop x = Quantified {runQuantified :: Nat x -> prop x}
+
+induction ::
+   quant Zero -> (forall x. Nat x -> quant (Succ x)) ->
+   Nat y -> quant y
+induction base step y@Nat =
+   runQuantified
+      (switchNat
+         (Quantified $ const base)
+         (Quantified $ step . prevNat))
+      y
+
+
+data AddZeroL x = (Zero:+:x) ~ x => AddZeroL
+
+succZeroL :: AddZeroL x -> AddZeroL (Succ x)
+succZeroL AddZeroL = AddZeroL
+
+addZeroL :: Nat x -> AddZeroL x
+addZeroL = induction AddZeroL (succZeroL . addZeroL)
+
+
+{-
+induction step:
+
+Succ x :+: Succ y
+Succ (x :+: Succ y)
+Succ (Succ (x:+:y))
+Succ (Succ x :+: y)
+-}
+data AddSuccL x y = (Succ x :+: y) ~ Succ (x:+:y) => AddSuccL
+
+succSuccL :: AddSuccL x y -> AddSuccL x (Succ y)
+succSuccL AddSuccL = AddSuccL
+
+addSuccL :: Nat x -> Nat y -> AddSuccL x y
+addSuccL x =
+   induction
+      (case addZeroL x of AddZeroL -> AddSuccL)
+      (succSuccL . addSuccL x)
+
+
+{-
+induction step:
+
+y :+: Succ x
+Succ (y :+: x)
+Succ (x :+: y)
+Succ x :+: y
+-}
+data AddComm x y = (x:+:y) ~ (y:+:x) => AddComm
+
+succComm :: Nat x -> Nat y -> AddComm x y -> AddComm x (Succ y)
+succComm x y AddComm = case addSuccL y x of AddSuccL -> AddComm
+
+{- |
+The proof is pretty expensive.
+For proving (x:+:y ~ y:+:x) we need about @x*y@ reduction steps.
+-}
+addComm :: Nat x -> Nat y -> AddComm x y
+addComm x =
+   induction
+      (case addZeroL x of AddZeroL -> AddComm)
+      (\y -> succComm x y $ addComm x y)
+
+
+{-
+induction step:
+
+x :+: (y :+: Succ z)
+x :+: Succ (y :+: z)
+Succ (x :+: (y :+: z))
+Succ ((x :+: y) :+: z)
+(x :+: y) :+: Succ z
+-}
+data AddAssoc x y z = (x:+:(y:+:z)) ~ ((x:+:y):+:z) => AddAssoc
+
+succAssoc :: AddAssoc x y z -> AddAssoc x y (Succ z)
+succAssoc AddAssoc = AddAssoc
+
+addAssoc :: Nat x -> Nat y -> Nat z -> AddAssoc x y z
+addAssoc x y = induction AddAssoc (succAssoc . addAssoc x y)
+
+
 newtype
-   MulNatTheorem x y =
-      MulNatTheorem {
-         runMulNatTheorem :: Nat x -> Nat y -> Nat (x :*: y)
-      }
+   QuantifiedMul condx condy prop x y =
+      QuantifiedMul {runQuantifiedMul :: condx x -> condy y -> prop (x :*: y)}
 
 mulNat :: Nat x -> Nat y -> Nat (x :*: y)
 mulNat x0 y0@Nat =
-   runMulNatTheorem
+   runQuantifiedMul
       (switchNat
-         (MulNatTheorem $ \Nat Nat -> Nat)
-         (MulNatTheorem $ \x -> addNat x . mulNat x . prevNat))
+         (QuantifiedMul $ \Nat Nat -> Nat)
+         (QuantifiedMul $ \x -> addNat x . mulNat x . prevNat))
       x0 y0
 
-
-newtype
-   MulPosTheorem x y =
-      MulPosTheorem {
-         runMulPosTheorem :: Pos x -> Pos y -> Pos (x :*: y)
-      }
-
 mulPos :: Pos x -> Pos y -> Pos (x :*: y)
 mulPos x0 y0@Pos =
-   runMulPosTheorem
+   runQuantifiedMul
       (switchPos
-         (MulPosTheorem $ \x ->
-            addPosL x . mulNat (natFromPos x) . prevPos))
+         (QuantifiedMul $ \x -> addPosL x . mulNat (natFromPos x) . prevPos))
       x0 y0
diff --git a/tfp.cabal b/tfp.cabal
--- a/tfp.cabal
+++ b/tfp.cabal
@@ -1,5 +1,5 @@
 name:           tfp
-version:        1.0.0.2
+version:        1.0.1
 build-type:     Simple
 license:        BSD3
 license-file:   LICENSE
@@ -18,16 +18,16 @@
   and functions on numerical values at compile time.
 category:       Type System
 tested-with:    GHC == 7.4.2, GHC == 7.6.3, GHC == 7.8.4, GHC == 8.0.1
-cabal-version:  >= 1.14
+cabal-version:  1.14
 extra-source-files:
-  CHANGES
+  Changes.md
 
 source-repository head
   type:         darcs
   location:     http://hub.darcs.net/thielema/tfp/
 
 source-repository this
-  tag:          1.0.0.2
+  tag:          1.0.1
   type:         darcs
   location:     http://hub.darcs.net/thielema/tfp/