diff --git a/free-theorems.cabal b/free-theorems.cabal
--- a/free-theorems.cabal
+++ b/free-theorems.cabal
@@ -1,5 +1,5 @@
 name:           free-theorems
-version:        0.2.1
+version:        0.3
 license:        PublicDomain
 license-file:   LICENSE
 author:         Sascha Boehme
@@ -47,6 +47,7 @@
     Language.Haskell.FreeTheorems.PrettyBase
     Language.Haskell.FreeTheorems.PrettyTypes
     Language.Haskell.FreeTheorems.PrettyTheorems
+    Language.Haskell.FreeTheorems.Theorems.Simplify
 hs-source-dirs: src
 extensions:     Generics, DeriveDataTypeable, Rank2Types, PatternSignatures
 extra-source-files:
diff --git a/src/Language/Haskell/FreeTheorems.hs b/src/Language/Haskell/FreeTheorems.hs
--- a/src/Language/Haskell/FreeTheorems.hs
+++ b/src/Language/Haskell/FreeTheorems.hs
@@ -41,6 +41,8 @@
 --   (7) Optional: Extract class constraints to show their definition
 --       ('unfoldClasses') and pretty-print them ('prettyUnfoldedClass').
 --
+--   (8) Optional: Further simplify the Formulas ('simplify') or UnfoldedLift
+--       ('simplifyUnfoldedLift') by syntactic transformations.
 
 module Language.Haskell.FreeTheorems (
 
@@ -77,7 +79,14 @@
   , unfoldLifts
   , unfoldClasses
 
+    -- * Simplifications
+    --
+    -- | These syntactic transformations are only valid for equational theorems
+    --   in the basic subset or the subset with fix, as eta reduction will be tried.
 
+  , simplify
+  , simplifyUnfoldedLift
+
     -- * Pretty printing
     
     -- | The pretty printer is based on the module \"Text.PrettyPrint\" which
@@ -104,6 +113,7 @@
 import Language.Haskell.FreeTheorems.LanguageSubsets
 import Language.Haskell.FreeTheorems.Intermediate
 import Language.Haskell.FreeTheorems.Theorems
+import Language.Haskell.FreeTheorems.Theorems.Simplify
 import Language.Haskell.FreeTheorems.Unfold
 import Language.Haskell.FreeTheorems.PrettyTypes
 import Language.Haskell.FreeTheorems.PrettyTheorems
diff --git a/src/Language/Haskell/FreeTheorems/BasicSyntax.hs b/src/Language/Haskell/FreeTheorems/BasicSyntax.hs
--- a/src/Language/Haskell/FreeTheorems/BasicSyntax.hs
+++ b/src/Language/Haskell/FreeTheorems/BasicSyntax.hs
@@ -1,4 +1,4 @@
-
+{-# LANGUAGE DeriveDataTypeable #-}
 
 
 -- | Declares the basic syntax of a Haskell98 subset enriched with 
diff --git a/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs b/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs
--- a/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs
+++ b/src/Language/Haskell/FreeTheorems/Frontend/TypeExpressions.hs
@@ -1,4 +1,4 @@
-
+{-# LANGUAGE ExistentialQuantification, Rank2Types #-}
 
 
 -- | Defines standard functions for modifying type expressions or retrieving
diff --git a/src/Language/Haskell/FreeTheorems/LanguageSubsets.hs b/src/Language/Haskell/FreeTheorems/LanguageSubsets.hs
--- a/src/Language/Haskell/FreeTheorems/LanguageSubsets.hs
+++ b/src/Language/Haskell/FreeTheorems/LanguageSubsets.hs
@@ -1,4 +1,4 @@
-
+{-# LANGUAGE DeriveDataTypeable #-}
 
 -- | Declares the available Haskell language subsets and the result types for
 --   generating free theorems. 
diff --git a/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs b/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs
--- a/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs
+++ b/src/Language/Haskell/FreeTheorems/PrettyTheorems.hs
@@ -252,8 +252,11 @@
   parensIf (withParens pc) $
     fsep [ prettyTerm (noParens pc) x, text "/=", text "_|_" ]
 
+prettyPredicate pc (IsTrue) = 
+  text "True"
 
 
+
 -- | Pretty-prints a term.
 
 prettyTerm :: PrettyControl -> Term -> Doc
@@ -268,6 +271,16 @@
       p = if withTypes then useParens else noParens
       pt = prettyTerm (useParens pc) t 
    in pt <> showInstantiation withTypes d
+
+prettyTerm pc (TermComp []) = 
+  text "id"
+
+prettyTerm pc (TermComp [t]) = 
+  parensIf (withParens pc) $ prettyTerm (noParens pc) t
+
+prettyTerm pc (TermComp (t:ts)) = 
+  parensIf (withParens pc) $ prettyTerm (noParens pc) t <+> text "." <+>
+                             prettyTerm (noParens pc) (TermComp ts)
 
 
 
diff --git a/src/Language/Haskell/FreeTheorems/Theorems.hs b/src/Language/Haskell/FreeTheorems/Theorems.hs
--- a/src/Language/Haskell/FreeTheorems/Theorems.hs
+++ b/src/Language/Haskell/FreeTheorems/Theorems.hs
@@ -1,4 +1,4 @@
-
+{-# LANGUAGE DeriveDataTypeable #-}
 
 
 -- | Data structures to describe theorems generated from types.
@@ -81,6 +81,9 @@
   
   | IsNotBot Term
         -- ^ The term is not equal to @_|_@.
+
+  | IsTrue
+        -- ^ Constant True Predicate
   
   deriving (Typeable, Data)
 
@@ -92,6 +95,7 @@
   = TermVar TermVariable            -- ^ A term variable.
   | TermIns Term TypeExpression     -- ^ Instantiation of a term.
   | TermApp Term Term               -- ^ Application of a term to a term.
+  | TermComp [Term]                 -- ^ Composition of function terms
   deriving (Typeable, Data, Eq)
 
 
diff --git a/src/Language/Haskell/FreeTheorems/Theorems/Simplify.hs b/src/Language/Haskell/FreeTheorems/Theorems/Simplify.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/FreeTheorems/Theorems/Simplify.hs
@@ -0,0 +1,150 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+
+module Language.Haskell.FreeTheorems.Theorems.Simplify
+	( simplify
+        , simplifyUnfoldedLift
+ 	)
+where
+
+import Data.Generics
+import Data.Generics.Aliases
+import Data.Generics.Schemes
+import Data.Generics.Text (gshow)
+
+import Language.Haskell.FreeTheorems.Theorems
+
+simplify :: Formula -> Formula
+simplify f = gsimplify f
+
+simplifyUnfoldedLift :: UnfoldedLift -> UnfoldedLift
+simplifyUnfoldedLift l = gsimplify l
+
+
+-- Generics stuff:
+
+type ScopeInfo = [TermVariable]
+
+gsimplify :: Data d => (d -> d)
+gsimplify = everywhereScoped (\s -> id
+				    `extT` simplifyTerm
+                                    `extT` simplifyPredicate
+                                    `extT` simplifyFormula s
+			     ) []
+
+everywhereScoped :: (ScopeInfo -> GenericT) -> ScopeInfo -> GenericT
+everywhereScoped = everywhereContext gupdateScope
+
+-- Remember variables in scope
+
+gupdateScope :: (ScopeInfo -> GenericQ ScopeInfo)
+gupdateScope s = s `mkQ` flip updateScopeFormula s
+
+-- This will remember all variables currently in scope
+updateScopeFormula :: Formula -> ScopeInfo -> ScopeInfo
+updateScopeFormula (ForallFunctions (Left  tv) _ _ _) = (tv:)
+updateScopeFormula (ForallFunctions (Right tv) _ _ _) = (tv:)
+updateScopeFormula (ForallVariables tv _ _)           = (tv:)
+updateScopeFormula _                                  = id
+
+
+-- Simplificatoins
+
+simplifyFormula :: ScopeInfo -> Formula -> Formula
+
+-- Remove unused quantified variables
+simplifyFormula	_ (ForallVariables tv _ f) | not (tv `occursIn` f) = f
+ 
+-- ∀v.f v == g v ⇒ f == g
+simplifyFormula	_ (ForallVariables tv _ (Predicate (t1 `IsEqual` t2)))
+                                           | Just (f1,v1) <- toFunApp t1
+                                           , Just (f2,v2) <- toFunApp t2
+                                           , v1 == v2
+				           , (TermVar tv) == v1
+                                           = gsimplify $ Predicate (f1 `IsEqual` f2)
+ 
+-- Find definitions, and apply as far as possible
+simplifyFormula s (ForallVariables tv t f) | [def] <- possibleDefs tv f
+		  	                   = gsimplify $ -- Will loop if the definition
+                                                         -- would not remove itself
+					        ForallVariables tv t
+                                                (replaceTerm s (TermVar tv) def f)
+-- Remove empty Implication
+simplifyFormula _ (Implication (Predicate IsTrue) f) 
+                                           = f
+
+-- Nothing to optimize
+simplifyFormula _ f                        = f
+
+simplifyPredicate :: Predicate -> Predicate
+
+-- Remove tautologies
+simplifyPredicate (IsEqual t1 t2) | t1 == t2
+                                  = IsTrue
+
+{- This is wrong: The variable might be constrained:
+
+-- Eta reduction on both sides of an equality
+simplifyPredicate (IsEqual t1 t2) | Just (f1,v1) <- toFunApp t1
+                                  , Just (f2,v2) <- toFunApp t2
+                                  , v1 == v2
+                                  = gsimplify (IsEqual f1 f2) -- run simplification again
+-}
+
+-- Nothing to optimize
+simplifyPredicate p               = p
+
+
+simplifyTerm :: Term -> Term
+
+-- Simplify function concatenations
+simplifyTerm (TermComp [f]) = f
+simplifyTerm (TermComp (f : (TermComp fs) : r))
+                            = gsimplify (TermComp (f:fs ++ r))
+
+-- Nothing to optimize
+simplifyTerm t                = t
+	
+
+-- Actions
+
+replaceTerm :: ScopeInfo -> Term -> Term -> GenericT
+replaceTerm s0 t def = everywhereScoped (\s -> mkT (repl s)) s0
+  where repl :: ScopeInfo -> Term -> Term
+        repl s term | term == t
+                    , null (listify (not . (`elem` s)) def)
+                    = def
+                    | otherwise
+                    = term
+
+-- Inspections
+
+toFunApp :: Term -> Maybe (Term, Term)
+toFunApp (TermApp f v) | Just (fs,v') <- toFunApp v
+                       = Just (TermComp [f,fs],v')
+toFunApp (TermApp f v) = Just (f,v)
+toFunApp _             = Nothing
+
+occursIn :: (Typeable a, Data a1, Eq a) => a -> a1 -> Bool
+e `occursIn` e' = gAny (==e) e'
+
+possibleDefs :: TermVariable -> GenericQ [Term]
+possibleDefs tv a = everything (.) (id `mkQ` test) a []
+  where test (t1 `IsEqual` t2) | t1 == (TermVar tv) = (t2:)
+                               | t2 == (TermVar tv) = (t1:)
+        test _                 =  id
+
+-- Generic functions
+
+gAny :: Typeable b => (b -> Bool) -> GenericQ Bool
+gAny p = everything (||) (False `mkQ` p)
+
+-- | Extend version of 'everywhere', which keeps information about the context around
+everywhereContext :: (ctx -> GenericQ ctx) -> 
+	             (ctx -> GenericT) ->
+                      ctx ->
+		      GenericT
+everywhereContext ctxUpdate f ctx d
+	= let ctx' = ctxUpdate ctx d
+          in f ctx (gmapT (everywhereContext ctxUpdate f ctx') d)
+
+
diff --git a/src/Language/Haskell/FreeTheorems/Unfold.hs b/src/Language/Haskell/FreeTheorems/Unfold.hs
--- a/src/Language/Haskell/FreeTheorems/Unfold.hs
+++ b/src/Language/Haskell/FreeTheorems/Unfold.hs
@@ -1,4 +1,4 @@
-
+{-# LANGUAGE PatternSignatures #-}
 
 
 module Language.Haskell.FreeTheorems.Unfold (