diff --git a/MemoTrie.cabal b/MemoTrie.cabal
--- a/MemoTrie.cabal
+++ b/MemoTrie.cabal
@@ -1,5 +1,5 @@
 Name:                MemoTrie
-Version:             0.1
+Version:             0.2
 Cabal-Version:       >= 1.2
 Synopsis:            Trie-based memo functions
 Category:            Data
diff --git a/src/Data/MemoTrie.hs b/src/Data/MemoTrie.hs
--- a/src/Data/MemoTrie.hs
+++ b/src/Data/MemoTrie.hs
@@ -66,35 +66,99 @@
 instance HasTrie () where
     data () :->: a = UnitTrie a
     trie f = UnitTrie (f ())
-    untrie (UnitTrie x) () = x
+    untrie (UnitTrie a) = const a
 
+-- untrie (trie f)
+--  == untrie (UnitTrie (f ()))                            -- trie def
+--  == const (f ())                                        -- untrie def
+--  == f                                                   -- const-unit
+
+-- trie (untrie (UnitTrie a))
+--  == trie (const a)                                      -- untrie def
+--  == UnitTrie (const a ())                               -- trie def
+--  == UnitTrie a                                          -- const
+
+
 instance HasTrie Bool where
-    data Bool :->: a = BoolTrie a a
+    data Bool :->: x = BoolTrie x x
     trie f = BoolTrie (f False) (f True)
-    untrie (BoolTrie f _) False = f
-    untrie (BoolTrie _ t) True  = t
+    untrie (BoolTrie f t) = if' f t
 
+
+-- | Conditional with boolean last.
+-- Spec: @if' (f False) (f True) == f@
+if' :: x -> x -> Bool -> x
+if' f _ False = f
+if' _ t True  = t
+
+-- untrie (trie f)
+--  == untrie (BoolTrie (f False) (f True))                -- trie def
+--  == if' (f False) (f True)                              -- untrie def
+--  == f                                                   -- if' spec
+
+-- trie (untrie (BoolTrie f t))
+--  == trie (if' f t)                                      -- untrie def
+--  == BoolTrie (if' f t False) (if' f t True)             -- trie def
+--  == BoolTrie f t                                        -- if' spec
+
+
 instance (HasTrie a, HasTrie b) => HasTrie (Either a b) where
     data (Either a b) :->: x = EitherTrie (a :->: x) (b :->: x)
-    untrie (EitherTrie f g) = either (untrie f) (untrie g)
     trie f = EitherTrie (trie (f . Left)) (trie (f . Right))
+    untrie (EitherTrie s t) = either (untrie s) (untrie t)
 
+-- untrie (trie f)
+--   == untrie (EitherTrie (trie (f . Left)) (trie (f . Right))) -- trie def
+--   == either (untrie (trie (f . Left))) (untrie (trie (f . Right))) -- untrie def
+--   == either (f . Left) (f . Right)                      -- untrie . trie
+--   == f                                                  -- either
+
+-- trie (untrie (EitherTrie s t))
+--   == trie (either (untrie s) (untrie t))                -- untrie def
+--   == EitherTrie (trie (either (untrie s) (untrie t) . Left)) -- trie def
+--                 (trie (either (untrie s) (untrie t) . Right))
+--   == EitherTrie (trie (untrie s)) (trie (untrie t))     -- either
+--   == EitherTrie s t                                     -- trie . untrie
+
+
+
 instance (HasTrie a, HasTrie b) => HasTrie (a,b) where
     data (a,b) :->: x = PairTrie (a :->: (b :->: x))
-    trie f = PairTrie $ trie $ \a -> trie $ \b -> f (a,b)
+    trie f = PairTrie (trie (trie . curry f))
     untrie (PairTrie t) = uncurry (untrie .  untrie t)
 
-trip :: ((a,b),c) -> (a,b,c)
-trip ((a,b),c) = (a,b,c)
+-- untrie (trie f)
+--  == untrie (PairTrie (trie (trie . curry f)))           -- trie def
+--  == uncurry (untrie . untrie (trie (trie . curry f)))   -- untrie def
+--  == uncurry (untrie . trie . curry f)                   -- untrie . trie
+--  == uncurry (curry f)                                   -- untrie . untrie
+--  == f                                                   -- uncurry . curry
 
-detrip :: (a,b,c) -> ((a,b),c)
-detrip (a,b,c) = ((a,b),c)
+-- trie (untrie (PairTrie t))
+--  == trie (uncurry (untrie .  untrie t))                 -- untrie def
+--  == PairTrie (trie (trie . curry (uncurry (untrie .  untrie t)))) -- trie def
+--  == PairTrie (trie (trie . untrie .  untrie t))         -- curry . uncurry
+--  == PairTrie (trie (untrie t))                          -- trie . untrie
+--  == PairTrie t                                          -- trie . untrie
 
+
 instance (HasTrie a, HasTrie b, HasTrie c) => HasTrie (a,b,c) where
     data (a,b,c) :->: x = TripleTrie (((a,b),c) :->: x)
     trie f = TripleTrie (trie (f . trip))
     untrie (TripleTrie t) = untrie t . detrip
 
+trip :: ((a,b),c) -> (a,b,c)
+trip ((a,b),c) = (a,b,c)
+
+detrip :: (a,b,c) -> ((a,b),c)
+detrip (a,b,c) = ((a,b),c)
+
+
+instance HasTrie x => HasTrie [x] where
+    data [x] :->: a = ListTrie (Either () (x,[x]) :->: a)
+    trie f = ListTrie (trie (f . list))
+    untrie (ListTrie t) = untrie t . delist
+
 list :: Either () (x,[x]) -> [x]
 list = either (const []) (uncurry (:))
 
@@ -102,15 +166,14 @@
 delist []     = Left ()
 delist (x:xs) = Right (x,xs)
 
-instance HasTrie x => HasTrie [x] where
-    data [x] :->: a = ListTrie (Either () (x,[x]) :->: a)
-    trie f = ListTrie (trie (f . list))
-    untrie (ListTrie t) = untrie t . delist
 
 -- TODO: make these definitions more systematic.
 
 
--- Handy for Bits types
+instance HasTrie Word where
+    data Word :->: a = WordTrie ([Bool] :->: a)
+    trie f = WordTrie (trie (f . unbits))
+    untrie (WordTrie t) = untrie t . bits
 
 -- | Extract bits in little-endian order
 bits :: Bits t => t -> [Bool]
@@ -127,10 +190,6 @@
 unbits [] = 0
 unbits (x:xs) = unbit x .|. shiftL (unbits xs) 1
 
-instance HasTrie Word where
-    data Word :->: a = WordTrie ([Bool] :->: a)
-    trie f = WordTrie (trie (f . unbits))
-    untrie (WordTrie t) = untrie t . bits
 
 -- Although Int is a Bits instance, we can't use bits directly for
 -- memoizing, because the "bits" function gives an infinite result, since