diff --git a/Induction/Structural.hs b/Induction/Structural.hs
new file mode 100644
--- /dev/null
+++ b/Induction/Structural.hs
@@ -0,0 +1,73 @@
+{- |
+
+This package aims to perform the fiddly details of instantiating induction
+schemas for algebraic data types. The library is parameterised over
+the type of variables (@v@), constructors (@c@) and types (@t@).
+
+Let's see how it looks if you instantiate all these three with String and want
+to do induction over natural numbers. First, one needs to create a type
+environment, a `TyEnv`. For every type (we only have one), we need to list its
+constructors. For each constructor, we need to list its arguments and whether
+they are recursive or not.
+
+>testEnv :: TyEnv String String
+>testEnv "Nat" = Just [ ("zero",[]) , ("succ",[Rec "Nat"]) ]
+>testEnv _ = Nothing
+
+Now, we can use the `subtermInduction` to get induction hypotheses which are
+just subterms of the conclusion. Normally, you would translate the `Term`s from
+the proof `Obligation`s to some other representation, but there is also
+linearisation functions included (`linObligations`, for instance.)
+
+>natInd :: [String] -> [Int] -> IO ()
+>natInd vars coords = putStrLn
+>    $ render
+>    $ linObligations strStyle
+>    $ unTag (\(x :~ i) -> x ++ show i)
+>    $ subtermInduction testEnv typed_vars coords
+>  where
+>    typed_vars = zip vars (repeat "Nat")
+
+The library will create fresh variables for you (called `Tagged` variables),
+but you need to remove them, using for instance `unTag`. If you want to sync
+it with your own name supply, use `unTagM` or `unTagMapM`.
+
+An example invocation:
+
+>*Mini> natInd ["X"] [0]
+>P(zero).
+>! [X1 : Nat] : (P(X1) => P(succ(X1))).
+
+This means to do induction on the zeroth coord (hence the @0@), and the variable
+is called "X". When using the library, it is up to you to translate the
+abstract @P@ predicate to something meaningful.
+
+We can also do induction on several variables:
+
+>*Mini> natInd ["X","Y"] [0,1]
+>P(zero,zero).
+>! [Y3 : Nat] : (P(zero,Y3) => P(zero,succ(Y3))).
+>! [X1 : Nat] : (P(X1,zero) => P(succ(X1),zero)).
+>! [X1 : Nat,Y3 : Nat] :
+>    (P(X1,Y3) &
+>    P(X1,succ(Y3)) &
+>    P(succ(X1),Y3)
+>     => P(succ(X1),succ(Y3))).
+
+In the last step case, all proper subterms of @succ(X1),succ(Y3)@ are used as
+hypotheses.
+
+A bigger example is in @example/Example.hs@ in the distribution.
+
+-}
+module Induction.Structural (
+    module Induction.Structural.Subterms,
+    module Induction.Structural.Types,
+    module Induction.Structural.Linearise
+) where
+
+import Induction.Structural.Subterms
+import Induction.Structural.Types
+import Induction.Structural.Linearise
+
+{-# ANN module "HLint: ignore Use import/export shortcut" #-}
diff --git a/Induction/Structural/Auxiliary.hs b/Induction/Structural/Auxiliary.hs
new file mode 100644
--- /dev/null
+++ b/Induction/Structural/Auxiliary.hs
@@ -0,0 +1,30 @@
+{-# OPTIONS_HADDOCK hide #-}
+-- | Internal auxiliary functions (pertaining to general haskell types)
+module Induction.Structural.Auxiliary where
+
+import Control.Monad (liftM)
+import Data.List     (sortBy, groupBy)
+import Data.Function (on)
+import Data.Ord      (comparing)
+
+-- | Concatenate the results after mapM
+concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
+concatMapM f = liftM concat . mapM f
+
+infixr 9 .:
+
+-- | Function composition deluxe
+--
+--   @(f .: g) = \x y -> f (g x y)@
+(.:) :: (b -> c) -> (a -> a' -> b) -> a -> a' -> c
+(.:) = (.) . (.)
+
+-- | /O(n log n)/ group, but destroys ordering
+groupSortedOn :: Ord b => (a -> b) -> [a] -> [[a]]
+groupSortedOn f = groupBy ((==) `on` f)
+                . sortBy (comparing f)
+
+-- | /O(n log n)/ nub by a comparison function. Destroys ordering
+nubSortedOn :: Ord b => (a -> b) -> [a] -> [a]
+nubSortedOn f = map head . groupSortedOn f
+
diff --git a/Induction/Structural/Linearise.hs b/Induction/Structural/Linearise.hs
new file mode 100644
--- /dev/null
+++ b/Induction/Structural/Linearise.hs
@@ -0,0 +1,93 @@
+-- | Linearisation
+{-# LANGUAGE RecordWildCards #-}
+module Induction.Structural.Linearise
+    (
+    -- * Linearising (pretty-printing) obligations and terms
+      linObligations,
+      linObligation,
+      linTerm,
+      Style(..),
+      strStyle,
+    -- ** Convenience re-export
+      render,
+      text
+    ) where
+
+import Induction.Structural.Types
+
+import Text.PrettyPrint hiding (Style)
+
+-- | Functions for linearising constructors (`linc`), variables (`linv`) and
+-- types (`lint`).
+data Style c v t = Style
+    { linc :: c -> Doc
+    , linv :: v -> Doc
+    , lint :: t -> Doc
+    }
+
+-- | An example style where constructors, variables and types are represented as `String`.
+strStyle :: Style String String String
+strStyle = Style
+    { linc = text
+    , linv = text
+    , lint = text
+    }
+
+-- | Linearises a list of `Obligation`, using a given `Style`.
+linObligations :: Style c v t -> [Obligation c v t] -> Doc
+linObligations s = vcat . map ((<> dot) . linObligation s)
+
+-- | Linearises an `Obligation` using a given `Style`. The output format is
+-- inspired by TPTP, but with typed quantifiers.
+linObligation :: Style c v t -> Obligation c v t -> Doc
+linObligation s@Style{..} x = case x of
+    Obligation sks []   concl -> linForall sks <+> linPred concl
+    Obligation sks hyps concl -> hang (linForall sks) 4 $
+        cat $ parList $
+            punctuate (fluff ampersand) (map linHyp hyps) ++
+            [space <> darrow <+> linPred concl]
+  where
+    linTypedVar v t = linv v <+> colon <+> lint t
+
+    linForall [] = empty
+    linForall qs =
+        bang <+> brackets (csv (map (uncurry linTypedVar) qs)) <+> colon
+
+    linPred xs = char 'P' <> parens (csv (map (linTerm s) xs))
+
+    linHyp ([],hyp) = linPred hyp
+    linHyp (qs,hyp) = parens (linForall qs <+> linPred hyp)
+
+-- | Linearises a `Term` using a given `Style`.
+linTerm :: Style c v t -> Term c v -> Doc
+linTerm Style{..} = go where
+    go tm = case tm of
+        Var v    -> linv v
+        Con c [] -> linc c
+        Con c ts -> linc c <> parens (csv (map go ts))
+        Fun v ts -> linv v <> parens (csv (map go ts))
+
+
+csv :: [Doc] -> Doc
+csv = hcat . punctuate comma
+
+parList :: [Doc] -> [Doc]
+parList []     = [parens empty]
+parList [x]    = [x]
+parList (x:xs) = (lparen <> x) : init xs ++ [last xs <> rparen]
+
+ampersand :: Doc
+ampersand = char '&'
+
+bang :: Doc
+bang = char '!'
+
+fluff :: Doc -> Doc
+fluff d = space <> d <> space
+
+darrow :: Doc
+darrow = text "=>"
+
+dot :: Doc
+dot = char '.'
+
diff --git a/Induction/Structural/Subterms.hs b/Induction/Structural/Subterms.hs
new file mode 100644
--- /dev/null
+++ b/Induction/Structural/Subterms.hs
@@ -0,0 +1,210 @@
+-- | Induction with subterms as hypotheses
+{-# LANGUAGE ParallelListComp, ScopedTypeVariables #-}
+module Induction.Structural.Subterms
+    (
+    -- * Induction with subterms as hypotheses
+      subtermInduction,
+    -- * Case analysis (no induction hypotheses)
+      caseAnalysis
+    ) where
+
+import Control.Applicative
+import Control.Arrow (first)
+import Control.Monad.State
+
+import Data.Maybe
+
+import Induction.Structural.Auxiliary (concatMapM,nubSortedOn)
+import Induction.Structural.Types
+import Induction.Structural.Utils
+
+import Safe
+
+-- | Find the type of a variable using the index in a type environment
+mfindVNote :: String -> Tagged a -> [(Tagged a,t)] -> t
+mfindVNote note u = snd . headNote note . filter (\ (v,_) -> tag u == tag v)
+
+-- We annotate constructors in the terms with the types of the arguments they
+-- have to easily be able to calculate subterms
+type C c t = (c,[Arg t])
+
+-- Term and terms explicitly quantified with variables
+type QuantTerm c v t = ([(Tagged v,t)],TaggedTerm (C c t) v)
+type QuantTerms c v t = ([(Tagged v,t)],[TaggedTerm (C c t) v])
+
+-- Given
+--
+--      [ [ all x0 . P (tx0) , all x1 . P(tx1) ]
+--      , [ all y0 . P (ty0) , all y1 . P(ty1) ]
+--      ]
+--
+-- Returns
+--
+--      [ all x0 y0 . P (tx0,ty0)
+--      , all x0 y1 . P (tx0,ty1)
+--      , all x1 y0 . P (tx1,ty0)
+--      , all x1 y1 . P (tx1,ty1)
+--      ]
+--
+-- Assumption: x0, x1, y0, y1 are all different
+makeQuantTerms :: [[QuantTerm c v t]] -> [QuantTerms c v t]
+makeQuantTerms qtmss =
+    [ (concat qs,tms)
+    | qtms <- sequence qtmss
+    , let (qs,tms) = unzip qtms
+    ]
+
+-- | Instantiate a variable with a given type, returning the new variables and
+--   what the term should be replaced with
+inst :: forall c v t . TyEnv c t -> Tagged v -> t -> Fresh (Maybe [QuantTerm c v t])
+inst env v t = case env t of
+    Just ks -> Just <$> mapM (uncurry inst') ks
+    Nothing -> return Nothing
+  where
+    inst' :: c -> [Arg t] -> Fresh (QuantTerm c v t)
+    inst' k as = do
+        args <- mapM (refreshTypedTagged v . argRepr) as
+        return (args,Con (k,as) [ Var x | (x,_) <- args ])
+
+-- | Induction on every variable in a term
+--
+-- Assumption: The variables only occur once in each term.
+inductionTm :: forall c v t .
+               TyEnv c t -> QuantTerm c v t -> Fresh [QuantTerm c v t]
+inductionTm env (qs0,tm0) = go tm0
+  where
+    go :: TaggedTerm (C c t) v -> Fresh [QuantTerm c v t]
+    go tm = case tm of
+        Var x@(_ :~ x_idx) -> do
+            let ty = headNote "inductionTm: unbound variable!"
+                     [ t | (_ :~ idx,t) <- qs0, x_idx == idx ]
+            fromMaybe [([(x,ty)],tm)] <$> inst env x ty
+        Con c tms -> goTms (Con c) tms
+        Fun f tms -> goTms (Fun f) tms
+
+    goTms :: ([TaggedTerm (C c t) v] -> TaggedTerm (C c t) v) ->
+             [TaggedTerm (C c t) v] -> Fresh [QuantTerm c v t]
+    goTms mk tms0 = do
+        qtmss <- mapM go tms0
+        return [ (qs,mk tms) | (qs,tms) <- makeQuantTerms qtmss ]
+
+-- | Induction several times on a variable
+repeatInductionTm :: forall c v t . TyEnv c t -> v -> t -> Int -> Fresh [QuantTerm c v t]
+repeatInductionTm env v t n0 = do
+    vv <- newTyped v t
+    go n0 [([vv],Var (fst vv))]
+  where
+    go :: Int -> [QuantTerm c v t] -> Fresh [QuantTerm c v t]
+    go 0 qtms = return qtms
+    go n qtms = concatMapM (go (n - 1) <=< inductionTm env) qtms
+
+-- | Unroll to a given depth, but does not add any hypotheses
+noHyps :: forall c v t . TyEnv c t -> [(v,t)] -> [Int]
+       -> Fresh [TaggedObligation (C c t) v t]
+noHyps env vars coords = do
+    obligs <- sequence
+        [ repeatInductionTm env v t (length (filter (ix ==) coords))
+        | (v,t) <- vars
+        | ix <- [0..]
+        ]
+    return $ makeObligations (makeQuantTerms obligs)
+
+-- | Make Obligations: this means to add empty hypotheses to QuantTerms.
+makeObligations :: [QuantTerms c v t] -> [TaggedObligation (C c t) v t]
+makeObligations qtms = [ Obligation qs [] tms | (qs,tms) <- qtms ]
+
+-- | Removes the argument type information from the constructors
+removeArgs :: [Obligation (C c t) v t] -> [Obligation c v t]
+removeArgs parts =
+    [ Obligation skolem [ (qs,map removeArg hyp) | (qs,hyp) <- hyps ]
+                        (map removeArg concl)
+    | Obligation skolem hyps concl <- parts
+    ]
+
+-- | Removes the argument type information from the constructors in one Term
+removeArg :: Term (C c t) v -> Term c v
+removeArg = go where
+    go tm = case tm of
+        Var x         -> Var x
+        Con (c,_) tms -> Con c (map go tms)
+        Fun f     tms -> Fun f (map go tms)
+
+-- | Does case analysis on a list of typed variables.  This function is equal
+-- to removing all the hypotheses from `subtermInduction`.
+caseAnalysis :: TyEnv c t -> [(v,t)] -> [Int] -> [TaggedObligation c v t]
+caseAnalysis env args = removeArgs . runFresh . noHyps env args
+
+-- | Gets all well-typed subterms of a term, including yourself.
+--
+-- The first argument is always yourself.
+--
+-- We need terms where the constructors are associated with their arguments.
+subterms :: Term (C c t) v -> [Term (C c t) v]
+subterms (Var x) = [Var x]
+subterms (Fun x tms) = Fun x tms : map (Fun x) (mapM subterms tms)
+subterms (Con c@(_,as) tms) = direct ++ indirect
+  where
+    -- Starting with this constructor. This includes the term we started with.
+    direct   = map (Con c) (mapM subterms tms)
+    -- Well-typed subterms of the arguments to the constructor
+    indirect = concat [ subterms tm | (Rec _,tm) <- zip as tms ]
+
+-- | Does this term contain a variable somewhere?
+hasVar :: Term c v -> Bool
+hasVar Var{} = True
+hasVar Fun{} = True
+hasVar (Con _ as) = any hasVar as
+
+-- | Adds hypotheses to an Obligation.
+--
+-- Important to drop 1, otherwise we get the conclusion as a hypothesis!
+--
+-- Hypotheses that only contain constructors (no variables) are removed.
+addHypotheses :: Ord c => TaggedObligation (C c t) v t -> TaggedObligation (C c t) v t
+addHypotheses (Obligation qs _ tms) = Obligation qs hyps tms
+  where
+    -- The empty lists denotes that we are not quantifying over any new
+    -- variables in the hypotheses.
+    hyps = nubSortedOn (map removeArg . snd)
+                       [ ([],h)
+                       | h <- drop 1 (mapM subterms tms)
+                       , any hasVar h
+                       ]
+
+-- | Adds hypotheses to an Obligation, requantifying over naked variables
+--
+-- I.e. forall x y . P(K x,y) becomes
+--      forall x y . (forall y'.P(x,y')) -> P (K x,y)
+--
+-- Important to drop 1, otherwise we get the conclusion as a hypothesis!
+addHypothesesQ :: Ord c => TaggedObligation (C c t) v t -> Fresh (TaggedObligation (C c t) v t)
+addHypothesesQ ip = do -- Obligation qs hyps tms
+
+    let Obligation qs hyps conc = addHypotheses ip
+
+        mk_msg = ("addHypothesesQ: " ++)
+        msg_unbound  = mk_msg "Unbound variable!"
+        msg_mismatch = mk_msg "Concrete hypotheses but abstract conclusion!"
+
+        -- tm is from a hypothesis, e from the conclusion.
+        -- If e is a variable, tm should be the same, and we requantify over it
+        addQ tm e = case e of
+            Var x@(_ :~ xi) -> case tm of
+                Var (_ :~ yi)
+                    | xi == yi -> do
+                        let t = mfindVNote msg_unbound x qs
+                        xt'@(x',_) <- refreshTypedTagged x t
+                        return ([xt'],Var x')
+                _ -> error msg_mismatch
+            _ -> return ([],tm)
+
+    hyps' <- forM hyps $ \ ([],tms) -> mapAndUnzipM (uncurry addQ) (zip tms conc)
+
+    return (Obligation qs (map (first concat) hyps') conc)
+
+-- | Subterm induction: the induction hypotheses will contain the proper
+-- subterms of the conclusion.
+subtermInduction :: Ord c => TyEnv c t -> [(v,t)] -> [Int] -> [TaggedObligation c v t]
+subtermInduction env args =
+    removeArgs . runFresh . (mapM addHypothesesQ <=< noHyps env args)
+
diff --git a/Induction/Structural/Types.hs b/Induction/Structural/Types.hs
new file mode 100644
--- /dev/null
+++ b/Induction/Structural/Types.hs
@@ -0,0 +1,184 @@
+-- | Types
+module Induction.Structural.Types
+    (
+    -- * Obligations
+      Obligation(..), TaggedObligation,
+      Predicate,
+      Hypothesis,
+    -- ** Terms
+      Term(..),
+    -- * Typing environment
+      TyEnv,
+    -- ** Arguments
+      Arg(..),
+    -- * Tagged (fresh) variables
+      Tagged(..), tag,
+    -- ** Removing tagged variables
+      unTag, unTagM, unTagMapM
+    ) where
+
+import Control.Monad.Identity
+import Control.Monad.State
+
+import Data.Function (on)
+
+import Data.Map (Map)
+import qualified Data.Map as M
+
+-- | The simple term language only includes variables, constructors and functions.
+data Term c v
+    = Var v
+    | Con c [Term c v]
+    | Fun v [Term c v]
+    -- ^ Induction on exponential data types yield assumptions with functions
+  deriving (Eq,Ord)
+
+-- Typed variables are represented as (v,t)
+
+-- | A list of terms.
+--
+-- Example: @[tm1,tm2]@ corresponds to the formula /P(tm1,tm2)/
+type Predicate c v = [Term c v]
+
+-- | Quantifier lists are represented as tuples of variables and their type.
+--
+-- Example:
+--
+--
+-- >Obligation
+-- >    { implicit   = [(x,t1),(y,t2)]
+-- >    , hypotheses = [([],[htm1,htm2])
+-- >                   ,([(z,t3)],[htm3,htm4])
+-- >                   ]
+-- >    , conclusion = [tm1,tm2]
+-- >    }
+--
+-- Corresponds to the formula:
+--
+-- /forall (x : t1) (y : t2) . (P(htm1,htm2) & (forall (z : t3) . P(htm3,htm4)) => P(tm1,tm2))/
+--
+-- The implicit variables (/x/ and /y/) can be viewed as skolemised, and use
+-- these three formulae instead:
+--
+-- /P(htm1,htm2)./
+--
+-- /forall (z : t3) . P(htm3,htm4)./
+--
+-- /~ P(tm1,tm2)./
+--
+data Obligation c v t = Obligation
+    { implicit   :: [(v,t)]
+    -- ^ Implicitly quantified variables (skolemised)
+    , hypotheses :: [Hypothesis c v t]
+    -- ^ Hypotheses, with explicitly quantified variables
+    , conclusion :: Predicate c v
+    -- ^ The induction conclusion
+    }
+
+-- | Quantifier lists are represented as tuples of variables and their type.
+--
+-- Example:
+--
+-- @([(x,t1),(y,t2)],[tm1,tm2])@
+--
+-- corresponds to the formula
+--
+-- /forall (x : t1) (y : t2) . P(tm1,tm2)/
+type Hypothesis c v t = ([(v,t)],Predicate c v)
+
+
+-- | An argument to a constructor can be recursive (`Rec`) or non-recursive
+-- (`NonRec`).  Induction hypotheses will be asserted for `Rec` arguments.
+--
+-- For instance, when doing induction on @[a]@, then @(:)@ has two arguments,
+-- @NonRec a@ and @Rec [a]@. On the other hand, if doing induction on @[Nat]@,
+-- then @(:)@ has @NonRec Nat@ and @Rec [Nat]@.
+--
+-- Data types can also be exponential. Consider
+--
+-- @data Ord = Zero | Succ Ord | Lim (Nat -> Ord)@
+--
+-- Here, the @Lim@ constructor is exponential. If we describe types and
+-- constructors with strings, the constructors for this data type is:
+--
+-- >[ ("Zero",[])
+-- >, ("Succ",[Rec "Ord"])
+-- >, ("Lim",[Exp ("Nat -> Ord") ["Nat"])
+-- >]
+--
+-- The first argument to `Exp` is the type of the function, and the second
+-- argument are the arguments to the function.
+data Arg t
+    = Rec t
+    | NonRec t
+    | Exp t [t]
+
+-- | Given a type, return either that you cannot do induction on is type
+-- (`Nothing`), or `Just` the constructors and a description of their arguments
+-- (see `Arg`).
+--
+-- The function /should instantiate type variables/. For instance, if you look
+-- up the type @[Nat]@, you should return the cons constructor with arguments
+-- @Nat@ and @[Nat]@ (see `Arg`).
+--
+-- Examples of types not possible to do induction on are function spaces and
+-- type variables. For these, return `Nothing`.
+type TyEnv c t = t -> Maybe [(c,[Arg t])]
+
+-- | Cheap way of introducing fresh variables. The `Eq` and `Ord` instances
+-- only uses the `Integer` tag.
+data Tagged v = v :~ Integer
+
+-- | The `Integer` tag
+tag :: Tagged v -> Integer
+tag (_ :~ t) = t
+
+instance Eq (Tagged v) where
+    (==) = (==) `on` tag
+
+instance Ord (Tagged v) where
+    compare = compare `on` tag
+
+-- | Obligations with tagged variables (see `Tagged` and `unTag`)
+type TaggedObligation c v t = Obligation c (Tagged v) t
+
+-- | Removing tagged (fresh) variables in a monad.
+-- The remove function is exectued at /every occurence/ of a tagged variable.
+-- This is useful if you want to sync it with your own name supply monad.
+unTagM :: Monad m => (Tagged v -> m v') -> [TaggedObligation c v t] -> m [Obligation c v' t]
+unTagM f = mapM $ \ (Obligation skolem hyps concl) ->
+    Obligation <$> unQuant skolem
+               <*> mapM (\(qs,hyp) -> (,) <$> unQuant qs <*> mapM unTm hyp) hyps
+               <*> mapM unTm concl
+  where
+    (<$>) = liftM
+    (<*>) = ap
+
+    unQuant = mapM (\(v,t) -> (,) <$> f v <*> return t)
+
+    unTm tm = case tm of
+        Var x     -> Var <$> f x
+        Con c tms -> Con c <$> mapM unTm tms
+        Fun x tms -> Fun <$> f x <*> mapM unTm tms
+
+-- | Removing tagged (fresh) variables
+unTag :: (Tagged v -> v') -> [TaggedObligation c v t] -> [Obligation c v' t]
+unTag f = runIdentity . unTagM (return . f)
+
+-- | Remove tagged (fresh) variables in a monad.
+-- The remove function is exectued /only once/ for each tagged variable,
+-- and a `Map` of renamings is returned.
+-- This is useful if you want to sync it with your own name supply monad.
+unTagMapM :: Monad m => (Tagged v -> m v') -> [TaggedObligation c v t]
+         -> m ([Obligation c v' t],Map (Tagged v) v')
+unTagMapM f = flip runStateT M.empty . unTagM f'
+  where
+    f' tv = do
+        m <- get
+        case M.lookup tv m of
+            Just v' -> return v'
+            Nothing -> do
+                v' <- lift (f tv)
+                modify (M.insert tv v')
+                return v'
+
diff --git a/Induction/Structural/Utils.hs b/Induction/Structural/Utils.hs
new file mode 100644
--- /dev/null
+++ b/Induction/Structural/Utils.hs
@@ -0,0 +1,48 @@
+{-# OPTIONS_HADDOCK hide #-}
+-- | Internal utility functions (pertaining to data types in this library)
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+module Induction.Structural.Utils where
+
+import Control.Applicative hiding (empty)
+import Control.Monad.State
+
+import Induction.Structural.Types
+
+-- | Tagged terms
+type TaggedTerm c v = Term c (Tagged v)
+
+-- | Tagged hypotheses
+type TaggedHypothesis c v t = Hypothesis c (Tagged v) t
+
+-- | Get the representation of the argument
+argRepr :: Arg t -> t
+argRepr (Rec t)    = t
+argRepr (NonRec t) = t
+argRepr (Exp t _)  = t
+
+-- Fresh variables
+
+-- | A monad of fresh Integers
+newtype Fresh a = Fresh (State Integer a)
+  deriving (Functor,Applicative,Monad,MonadState Integer)
+
+-- | Run the fresh monad
+runFresh :: Fresh a -> a
+runFresh (Fresh m) = evalState m 0
+
+-- | Creating a fresh variable
+newFresh :: v -> Fresh (Tagged v)
+newFresh v = Fresh $ state $ \ s -> (v :~ s,s+1)
+
+-- | Create a fresh variable that has a type
+newTyped :: v -> t -> Fresh (Tagged v,t)
+newTyped v t = flip (,) t <$> newFresh v
+
+-- | Refresh variable
+refreshTagged :: Tagged v -> Fresh (Tagged v)
+refreshTagged (v :~ _) = newFresh v
+
+-- | Refresh a variable that has a type
+refreshTypedTagged :: Tagged v -> t -> Fresh (Tagged v,t)
+refreshTypedTagged v t = flip (,) t <$> refreshTagged v
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,165 @@
+                  GNU LESSER GENERAL PUBLIC LICENSE
+                       Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+
+  This version of the GNU Lesser General Public License incorporates
+the terms and conditions of version 3 of the GNU General Public
+License, supplemented by the additional permissions listed below.
+
+  0. Additional Definitions. 
+
+  As used herein, "this License" refers to version 3 of the GNU Lesser
+General Public License, and the "GNU GPL" refers to version 3 of the GNU
+General Public License.
+
+  "The Library" refers to a covered work governed by this License,
+other than an Application or a Combined Work as defined below.
+
+  An "Application" is any work that makes use of an interface provided
+by the Library, but which is not otherwise based on the Library.
+Defining a subclass of a class defined by the Library is deemed a mode
+of using an interface provided by the Library.
+
+  A "Combined Work" is a work produced by combining or linking an
+Application with the Library.  The particular version of the Library
+with which the Combined Work was made is also called the "Linked
+Version".
+
+  The "Minimal Corresponding Source" for a Combined Work means the
+Corresponding Source for the Combined Work, excluding any source code
+for portions of the Combined Work that, considered in isolation, are
+based on the Application, and not on the Linked Version.
+
+  The "Corresponding Application Code" for a Combined Work means the
+object code and/or source code for the Application, including any data
+and utility programs needed for reproducing the Combined Work from the
+Application, but excluding the System Libraries of the Combined Work.
+
+  1. Exception to Section 3 of the GNU GPL.
+
+  You may convey a covered work under sections 3 and 4 of this License
+without being bound by section 3 of the GNU GPL.
+
+  2. Conveying Modified Versions.
+
+  If you modify a copy of the Library, and, in your modifications, a
+facility refers to a function or data to be supplied by an Application
+that uses the facility (other than as an argument passed when the
+facility is invoked), then you may convey a copy of the modified
+version:
+
+   a) under this License, provided that you make a good faith effort to
+   ensure that, in the event an Application does not supply the
+   function or data, the facility still operates, and performs
+   whatever part of its purpose remains meaningful, or
+
+   b) under the GNU GPL, with none of the additional permissions of
+   this License applicable to that copy.
+
+  3. Object Code Incorporating Material from Library Header Files.
+
+  The object code form of an Application may incorporate material from
+a header file that is part of the Library.  You may convey such object
+code under terms of your choice, provided that, if the incorporated
+material is not limited to numerical parameters, data structure
+layouts and accessors, or small macros, inline functions and templates
+(ten or fewer lines in length), you do both of the following:
+
+   a) Give prominent notice with each copy of the object code that the
+   Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the object code with a copy of the GNU GPL and this license
+   document.
+
+  4. Combined Works.
+
+  You may convey a Combined Work under terms of your choice that,
+taken together, effectively do not restrict modification of the
+portions of the Library contained in the Combined Work and reverse
+engineering for debugging such modifications, if you also do each of
+the following:
+
+   a) Give prominent notice with each copy of the Combined Work that
+   the Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the Combined Work with a copy of the GNU GPL and this license
+   document.
+
+   c) For a Combined Work that displays copyright notices during
+   execution, include the copyright notice for the Library among
+   these notices, as well as a reference directing the user to the
+   copies of the GNU GPL and this license document.
+
+   d) Do one of the following:
+
+       0) Convey the Minimal Corresponding Source under the terms of this
+       License, and the Corresponding Application Code in a form
+       suitable for, and under terms that permit, the user to
+       recombine or relink the Application with a modified version of
+       the Linked Version to produce a modified Combined Work, in the
+       manner specified by section 6 of the GNU GPL for conveying
+       Corresponding Source.
+
+       1) Use a suitable shared library mechanism for linking with the
+       Library.  A suitable mechanism is one that (a) uses at run time
+       a copy of the Library already present on the user's computer
+       system, and (b) will operate properly with a modified version
+       of the Library that is interface-compatible with the Linked
+       Version. 
+
+   e) Provide Installation Information, but only if you would otherwise
+   be required to provide such information under section 6 of the
+   GNU GPL, and only to the extent that such information is
+   necessary to install and execute a modified version of the
+   Combined Work produced by recombining or relinking the
+   Application with a modified version of the Linked Version. (If
+   you use option 4d0, the Installation Information must accompany
+   the Minimal Corresponding Source and Corresponding Application
+   Code. If you use option 4d1, you must provide the Installation
+   Information in the manner specified by section 6 of the GNU GPL
+   for conveying Corresponding Source.)
+
+  5. Combined Libraries.
+
+  You may place library facilities that are a work based on the
+Library side by side in a single library together with other library
+facilities that are not Applications and are not covered by this
+License, and convey such a combined library under terms of your
+choice, if you do both of the following:
+
+   a) Accompany the combined library with a copy of the same work based
+   on the Library, uncombined with any other library facilities,
+   conveyed under the terms of this License.
+
+   b) Give prominent notice with the combined library that part of it
+   is a work based on the Library, and explaining where to find the
+   accompanying uncombined form of the same work.
+
+  6. Revised Versions of the GNU Lesser General Public License.
+
+  The Free Software Foundation may publish revised and/or new versions
+of the GNU Lesser General Public License from time to time. Such new
+versions will be similar in spirit to the present version, but may
+differ in detail to address new problems or concerns.
+
+  Each version is given a distinguishing version number. If the
+Library as you received it specifies that a certain numbered version
+of the GNU Lesser General Public License "or any later version"
+applies to it, you have the option of following the terms and
+conditions either of that published version or of any later version
+published by the Free Software Foundation. If the Library as you
+received it does not specify a version number of the GNU Lesser
+General Public License, you may choose any version of the GNU Lesser
+General Public License ever published by the Free Software Foundation.
+
+  If the Library as you received it specifies that a proxy can decide
+whether future versions of the GNU Lesser General Public License shall
+apply, that proxy's public statement of acceptance of any version is
+permanent authorization for you to choose that version for the
+Library.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,4 @@
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain
diff --git a/structural-induction.cabal b/structural-induction.cabal
new file mode 100644
--- /dev/null
+++ b/structural-induction.cabal
@@ -0,0 +1,64 @@
+name:               structural-induction
+category:           Theorem Provers, Logic
+version:            0.1
+license:            LGPL-3
+license-file:       LICENSE
+author:             Dan Rosén
+maintainer:         Dan Rosén <danr@chalmers.se>
+homepage:           http://www.github.com/danr/structural-induction
+bug-reports:        http://www.github.com/danr/structural-induction/issues
+build-type:         Simple
+cabal-version:      >= 1.8
+tested-with:        GHC == 7.4.1, GHC == 7.6.1
+synopsis:           Instantiate structural induction schemas for algebraic data types
+description:        See documentation for Induction.Structural
+
+source-repository head
+  type: git
+  location: git://github.com/danr/structural-induction.git
+
+flag Werror
+  default: False
+  manual: True
+
+library
+  ghc-options:    -Wall
+  if flag(Werror)
+    ghc-options: -Werror
+
+  exposed-modules:
+    Induction.Structural,
+    Induction.Structural.Auxiliary,
+    Induction.Structural.Utils
+
+  other-modules:
+    Induction.Structural.Types,
+    Induction.Structural.Subterms,
+    Induction.Structural.Linearise
+
+  build-depends:
+    base                      >= 4 && < 5,
+    mtl,
+    containers,
+    pretty,
+    safe
+
+test-suite walk
+  type:           exitcode-stdio-1.0
+  main-is:        Main.hs
+  hs-source-dirs: test
+  ghc-options:    -Wall
+  if flag(Werror)
+    ghc-options: -Werror
+
+  build-depends:
+    structural-induction,
+    base,
+    pretty,
+    QuickCheck                >= 2.4,
+    mtl                       >= 2.1.2,
+    language-haskell-extract,
+    testing-feat              >= 0.4,
+    geniplate                 >= 0.6,
+    safe
+
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,135 @@
+{-# LANGUAGE TemplateHaskell, Rank2Types #-}
+module Main where
+
+import Control.Monad
+import Control.Applicative
+
+import Data.List
+import Data.Ord
+
+import System.Exit (exitFailure)
+
+import Test.QuickCheck
+import Test.QuickCheck.Test
+import Test.Feat.Access
+
+import Language.Haskell.Extract
+
+import Induction.Structural
+
+-- import Unsound
+
+import Trace
+import Env
+import EnvTypes
+import Walk
+import Util
+
+-- | Structural Induction Instatiator
+type SII = TyEnv Con' Ty' -> [(String,Ty')] -> [Int] -> [TaggedObligation Con' String Ty']
+
+-- | Do induction on a test case
+ind :: SII -> TestCase -> [Oblig]
+ind sii (TestCase types coords) =
+    unTag (\ (x :~ i) -> x ++ show i) $ sii testEnv' args coords
+  where
+    args = zip vars types
+
+    vars :: [String]
+    vars = concat [ replicateM n ['a'..'z'] | n <- [1..] ]
+
+data TestCase = TestCase [Ty'] [Int]
+  deriving Show
+
+unitTc :: Int -> [Int] -> TestCase
+unitTc n = TestCase (replicate n (Si Unit))
+
+boolTc :: Int -> [Int] -> TestCase
+boolTc x = TestCase (replicate x (Si Bool))
+
+natTc :: Int -> TestCase
+natTc x = TestCase [Si Nat] (replicate x 0)
+
+maybeTc :: Ty' -> Int -> Int -> TestCase
+maybeTc t d i = TestCase [repeatMaybe t d] (replicate i 0)
+
+repeatMaybe :: Ty' -> Int -> Ty'
+repeatMaybe t = go
+  where
+    go n | n <= 0    = t
+         | otherwise = case go (n - 1) of Si t' -> Si (Maybe t')
+
+mods :: Int -> [Int] -> [Int]
+mods 0 _  = []
+mods x xs = map (`mod` x) xs
+
+-- | Linear
+prop_units :: SII -> NonNegative Int -> [Int] -> Property
+prop_units sii (NonNegative x) xs
+    = mkProp sii (unitTc x' (mods x' xs))
+  where x' = min 5000 x
+
+-- | Can't try this too far because of exponential explosion
+prop_bools :: SII -> NonNegative Int -> [Int] -> Property
+prop_bools sii (NonNegative x) xs
+    = mkProp sii (boolTc x' (mods x' xs))
+  where x' = min 10 x
+
+-- | Linear
+prop_maybe :: SII -> NonNegative Int -> NonNegative Int -> Property
+prop_maybe sii (NonNegative d) (NonNegative i)
+    = mkProp sii (maybeTc (Si Unit) d' i')
+  where
+    d' = min 100 d
+    i' = min 100 i
+
+mkPropTy :: SII -> Ty' -> Int -> Property
+mkPropTy sii ty n = mkProp sii (TestCase [ty] (replicate n 0))
+
+mkProp :: SII -> TestCase -> Property
+mkProp sii tc@(TestCase tys _) =
+    forAllShrink (startFromTypes tys) (mapM shrinkRepr') $ \ start ->
+        forAll (makeTracer start parts) $ \ trace ->
+            case loop trace of
+                Just _  -> printTestCase (showOblig parts) False
+                Nothing -> property True
+  where parts = ind sii tc
+
+makeTestCases :: Integer -> IO [TestCase]
+makeTestCases tests = concat <$>
+    forM [0..tests] (\ ix -> do
+        let tys = indexWith enumTy's ix
+            all_coordss = concat [ coordss (length tys - 1) d | d <- [0..4] ]
+        coordss' <- head <$> sample' (shuffle all_coordss)
+        let css = nub . sortBy (comparing length) . sort . take 10 $ coordss'
+        return $ map (TestCase tys) css
+    )
+
+main :: IO ()
+main = do
+    let tests =
+            -- [("structuralInductionUnsound",structuralInductionUnsound)] ++
+            [("subtermInduction",subtermInduction,96)
+            ,("caseAnalysis",caseAnalysis,15)
+            ]
+    oks <- forM tests $ \ (name_sii,sii,test_depth) -> do
+        putStrLn $ "== " ++ name_sii ++ " =="
+
+        testcases <- makeTestCases test_depth
+        let num_tests = length testcases
+
+        ok_feat <- forM (zip testcases ([0..] :: [Integer])) $
+            \ (tc@(TestCase tys cs),i) -> do
+                putStrLn $ "(" ++ show i ++ "/" ++ show num_tests ++ ") " ++
+                           name_sii ++ ": " ++ show tys ++ " coords: " ++ show cs
+                quickCheckResult (mkProp sii tc)
+
+        ok_manual <- sequence $(functionExtractorMap "^prop_"
+            [| \ name_prop prop -> do
+                putStrLn $ name_sii ++ ": " ++ name_prop
+                quickCheckResult (prop sii) |])
+
+        return $ all isSuccess (ok_manual ++ ok_feat)
+
+    unless (and oks) exitFailure
+