diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,32 @@
+Copyright (c) 2005 Lennart Augustsson, Thomas Johnsson
+    Chalmers University of Technology
+All rights reserved.
+
+This code is derived from software written by Lennart Augustsson
+(lennart@augustsson.net).
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+3. None of the names of the copyright holders may be used to endorse
+   or promote products derived from this software without specific
+   prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
+BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
+WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
+OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
+IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+*** End of disclaimer. ***
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/djinn-th.cabal b/djinn-th.cabal
new file mode 100644
--- /dev/null
+++ b/djinn-th.cabal
@@ -0,0 +1,27 @@
+Name:                djinn-th
+Version:             0.0.1
+Synopsis:            Generate executable Haskell code from a type
+Description:         Djinn uses a theorem prover for intuitionistic
+                     propositional logic to generate a Haskell
+                     expression when given a type.
+                     .
+                     Djinn-TH uses Template Haskell to turn this
+                     expression into executable code.
+
+Homepage:            http://gitorious.org/djinn-th
+License:             BSD3
+License-file:        LICENSE
+Author:              Claude Heiland-Allen
+Maintainer:          claudiusmaximus@goto10.org
+Category:            Language
+Build-type:          Simple
+
+Cabal-version:       >=1.2
+
+Library
+  Hs-source-dirs:    src
+  Exposed-modules:   Language.Haskell.Djinn
+  Other-modules:     Language.Haskell.Djinn.LJT, Language.Haskell.Djinn.LJTFormula, Language.Haskell.Djinn.HTypes
+  Build-depends:     base >= 4 && < 5, template-haskell >= 2.4 && < 2.5, containers >= 0.3 && < 0.4, logict >= 0.4 && < 0.5
+  GHC-options:       -Wall
+  GHC-prof-options:  -prof -auto-all
diff --git a/src/Language/Haskell/Djinn.hs b/src/Language/Haskell/Djinn.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/Djinn.hs
@@ -0,0 +1,254 @@
+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Language.Haskell.Djinn
+-- License     :  BSD-style (see the accompanying LICENSE file)
+-- 
+-- Maintainer  :  claudiusmaximus@goto10.org
+-- Stability   :  experimental
+-- Portability :  non-portable (template-haskell)
+--
+-- Djinn uses a theorem prover for intuitionistic propositional logic to
+-- generate a Haskell expression when given a type. Djinn-TH uses Template
+-- Haskell to turn this expression into executable code.
+--
+-- Based mostly on <http://hackage.haskell.org/package/djinn>.
+--
+-- Using Language.Haskell.Djinn generally requires:
+--
+-- @&#x7B;-&#x23; LANGUAGE TemplateHaskell, ScopedTypeVariables &#x23;-&#x7D;@
+--
+-----------------------------------------------------------------------------
+
+--
+-- Modified to use TemplateHaskell by Claude Heiland-Allen, 2010
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module Language.Haskell.Djinn (
+  djinn,  -- :: Q Type -> Q Exp
+  djinns, -- :: Q Type -> Q Exp
+  djinnD, -- :: String -> Q Type -> Q [Dec]
+  djinnsD -- :: String -> Q Type -> Q [Dec]
+  ) where
+
+import Data.List (nub, sortBy)
+import Data.Ord (comparing)
+import Data.Ratio ((%))
+import Data.Set (Set, empty, singleton, union, toList)
+import Language.Haskell.TH (
+  Name, Type(..), Dec(..), Pat(..), Exp(..), Body(..), Clause(..),
+  Match(..), Info(..), Con(..), TyVarBndr(..), Q,
+  newName, mkName, tupleTypeName, tupleDataName, reify, pprint, report)
+import Control.Monad (forM)
+
+import Language.Haskell.Djinn.HTypes (
+  HType(..), HPat(..), HExpr(..), HClause(..), HEnvironment,
+  termToHClause, hTypeToFormula, getBinderVars)
+import Language.Haskell.Djinn.LJT (prove)
+
+getConTs :: Type -> Set Name
+getConTs (ForallT _ _ t) = getConTs t
+getConTs (ConT name)     = singleton name
+getConTs (AppT t1 t2)    = getConTs t1 `union` getConTs t2
+getConTs (TupleT n)      = singleton (tupleTypeName n)
+getConTs _               = empty
+
+hType :: Type -> HType
+hType (TupleT 0) = HTTuple []
+hType (TupleT 1)         = error $ "djinn: 1-tuple should not exist"
+-- FIXME kludge for now to handle small tuples...
+-- FIXME kludge to handle GHC's tuple stuff
+hType (AppT (AppT ArrowT t1) t2) = HTArrow (hType t1) (hType t2)
+hType (AppT (AppT (TupleT 2) t1) t2) = HTTuple (map hType [t1, t2])
+hType (AppT (AppT (ConT   c) t1) t2) | c == tupleTypeName 2 = HTTuple (map hType [t1, t2])
+hType (AppT (AppT (AppT (TupleT 3) t1) t2) t3) = HTTuple (map hType [t1, t2, t3])
+hType (AppT (AppT (AppT (ConT   c) t1) t2) t3) | c == tupleTypeName 3 = HTTuple (map hType [t1, t2, t3])
+hType (AppT (AppT (AppT (AppT (TupleT 4) t1) t2) t3) t4) = HTTuple (map hType [t1, t2, t3, t4])
+hType (AppT (AppT (AppT (AppT (ConT   c) t1) t2) t3) t4) | c == tupleTypeName 4 = HTTuple (map hType [t1, t2, t3, t4])
+hType (AppT (AppT (AppT (AppT (AppT (TupleT 5) t1) t2) t3) t4) t5) = HTTuple (map hType [t1, t2, t3, t4, t5])
+hType (AppT (AppT (AppT (AppT (AppT (ConT   c) t1) t2) t3) t4) t5) | c == tupleTypeName 5 = HTTuple (map hType [t1, t2, t3, t4, t5])
+hType (TupleT n) | n > 5 = error $ "djinn: " ++ show n ++ "-tuple not yet supported (max 5)"
+hType (AppT t1 t2) = HTApp (hType t1) (hType t2)
+hType (ForallT _ _ t) = hType t
+hType (VarT v) = HTVar v
+hType (ConT n) = HTCon n
+hType t = error $ "djinn: unimplemented in hType: " ++ pprint t
+
+-- two mutually recursive functions chase down all data/type defs
+
+environment :: Type -> Q HEnvironment
+environment = fmap concat . mapM environment1 . toList . getConTs
+
+environment1 :: Name -> Q HEnvironment
+environment1 name = do
+  info <- reify name
+  case info of
+   ClassI _dec -> fail $ "djinn: unexpected ClassI"
+   ClassOpI _n _t _c _fx -> fail $ "djinn: unexpected ClassOpI"
+   TyConI dec -> do
+    case dec of
+     DataD _cxt dName dVars dCtors _derivs -> do
+      dTypes <- forM dCtors $ \(NormalC cName cFields) -> do
+        let cTypes = map (hType . snd) cFields
+        cEnv <- mapM (environment . snd) cFields
+        return ((cName, cTypes), cEnv)
+      return $ [(dName, (map binderName dVars, HTUnion (map fst dTypes)))]
+             ++ (concat . concatMap snd $ dTypes)
+     TySynD tName tVars tType -> do
+      es <- environment tType
+      return $ [(tName, (map binderName tVars, hType tType))] ++ es
+     x -> fail $ "djinn: unexpected TyConI " ++ show x
+   PrimTyConI n _ar _l -> fail $ "djinn: unexpected PrimTyConI " ++ show n
+   DataConI _n _t _tn _fx -> fail $ "djinn: unexpected DataConI"
+   VarI _n _t _mdec _fx -> fail $ "djinn: unexpected VarI"
+   TyVarI _tvName _tvType -> fail $ "djinn: unexpected TyVarI"
+   
+binderName :: TyVarBndr -> Name
+binderName (PlainTV n) = n
+binderName (KindedTV n _k) = n
+
+pat :: HPat -> Pat
+pat (HPVar s) = VarP s
+pat (HPTuple ps) = TupP (map pat ps)
+pat (HPAt s p) = AsP s (pat p)
+pat (HPCon c) = ConP c []
+pat (HPApply p q) = let ConP c ps = pat p in ConP c (ps ++ [pat q])
+
+expr :: HExpr -> Exp
+expr (HELam ps e) = LamE (map pat ps) (expr e)
+expr (HEApply e f) = AppE (expr e) (expr f)
+expr (HECon c) = ConE c
+expr (HEVar v) = VarE v
+expr (HETuple es) = foldl AppE (ConE (tupleDataName (length es))) (map expr es)
+expr (HECase e ms) = CaseE (expr e) (map case1 ms)
+  where case1 (p, f) = Match (pat p) (NormalB $ expr f) []
+
+djinn0 :: Bool -> Maybe String -> Type -> Q Exp
+djinn0 multi mStr typ = do
+  syns <- environment typ
+  name <- case mStr of
+    Nothing -> newName "djinn"
+    Just s -> return $ mkName s
+  let form = hTypeToFormula syns (hType typ)
+  ps <- (nub . map snd . sortBy (comparing fst) . map (f name)) `fmap` (prove multi [] form)
+  if multi
+   then return $ ListE (map g ps)
+   else case  ps of
+    ps'@(p:_:_) -> do
+      report False $ "djinn: " ++ show (length ps') ++ " options for: " ++ show name ++ " :: " ++ pprint typ
+      return $ g p
+    [p] -> return $ g p
+    [] -> do
+      report True $ "djinn: cannot realize: " ++ show name ++ " :: " ++ pprint typ
+      x <- newName "djinnError"
+      return $ LetE [ValD (VarP x) (NormalB (VarE x)) [] ] (VarE x)
+  where
+    f name p  = let c = termToHClause name p
+                    bvs = getBinderVars c
+                    r = if null bvs then (0, 0) else (length (filter (== underscore) bvs) % length bvs, length bvs)
+                in  (r, c)
+    g (HClause _ pats body) = let e = expr (HELam pats body) in wilderE e
+
+underscore :: Name
+underscore = mkName "_"
+
+wilder :: Pat -> Pat
+wilder l@(LitP _) = l
+wilder (VarP n) | n == underscore = WildP
+wilder (TupP ps) = TupP (map wilder ps)
+wilder (ConP n ps) = ConP n (map wilder ps)
+wilder (InfixP p1 n p2) = InfixP (wilder p1) n (wilder p2)
+wilder (TildeP p) = TildeP (wilder p)
+wilder (AsP n p) | n == underscore = wilder p
+                 | otherwise = AsP n (wilder p)
+--wilder (RecP n fs) = error $ "djinn: field patterns not yet implemented"
+wilder (ListP ps) = ListP (map wilder ps)
+wilder (SigP p t) = SigP (wilder p) t
+wilder p = p
+
+wilderE :: Exp -> Exp
+wilderE (AppE e f) = AppE (wilderE e) (wilderE f)
+wilderE (InfixE me o mf) = InfixE (fmap wilderE me) (wilderE o) (fmap wilderE mf)
+wilderE (LamE ps e) = LamE (map wilder ps) (wilderE e)
+wilderE (TupE es) = TupE (map wilderE es)
+wilderE (CondE e f g) = CondE (wilderE e) (wilderE f) (wilderE g)
+wilderE (LetE ds e) = LetE (map wilderD ds) (wilderE e)
+wilderE (CaseE e ms) = CaseE (wilderE e) (map wilderM ms)
+-- DoE [Stmt]                         -- { do { p <- e1; e2 }  }
+-- CompE [Stmt]                       -- { [ (x,y) | x <- xs, y <- ys ] }
+-- ArithSeqE Range                    -- { [ 1 ,2 .. 10 ] }
+wilderE (ListE es) = ListE (map wilderE es)
+wilderE (SigE e t) = SigE (wilderE e) t
+-- RecConE Name [FieldExp]            -- { T { x = y, z = w } }
+-- RecUpdE Exp [FieldExp]             -- { (f x) { z = w } }
+wilderE e = e
+
+wilderM :: Match -> Match
+wilderM (Match p b ds) = Match (wilder p) (wilderB b) (map wilderD ds)
+
+wilderD :: Dec -> Dec
+wilderD d = d -- error "djinn: no wilderD yet"
+
+wilderB :: Body -> Body
+wilderB b = b --error "djinn: no wilderD yet"
+
+{- |
+Generate an anonymous expression of the given type (if it is realizable).
+-}
+djinn :: Q Type -- ^ type
+      -> Q Exp
+djinn qtyp = do
+  typ <- qtyp
+  djinn0 False Nothing typ
+
+{- |
+Generate a list of anonymous expressions of the given type (if it is realizable).
+-}
+djinns :: Q Type -- ^ type
+       -> Q Exp
+djinns qtyp = do
+  typ <- qtyp
+  djinn0 True Nothing typ
+
+{- |
+Generate a named declaration with an accompanying type signature.  For example:
+
+>   $(djinnD "maybeToEither" [t| forall a b . a ->  Maybe b ->  Either a b |])
+>   main = print . map (maybeToEither "foo") $ [ Nothing, Just "bar" ]
+
+might print @[Left \"foo\",Right \"bar\"]@.
+-}
+djinnD :: String  -- ^ name
+       -> Q Type  -- ^ type
+       -> Q [Dec]
+djinnD str qtyp = do
+  let name = mkName str
+  typ <- qtyp
+  exp' <- djinn0 False (Just str) typ
+  return
+    [ SigD name typ
+    , FunD name [ Clause [] (NormalB $ exp') [] ] ]
+
+{- |
+Generate a named declaration with an accompanying type signature
+for a list of possible realizations of a type.
+
+>   $(djinnsD "picks" [t| forall a . (a, a) -> (a -> a) -> a |])
+>   main = print [ p ("A","B") (++"C") | p <- picks ]
+
+might print @[\"BC\",\"AC\",\"B\",\"A\"]@.
+
+-}
+djinnsD :: String  -- ^ name
+        -> Q Type  -- ^ type
+        -> Q [Dec]
+djinnsD str qtyp = do
+  let name = mkName str
+  typ <- qtyp
+  exp' <- djinn0 True (Just str) typ
+  let ForallT vs cxt t = typ
+  return
+    [ SigD name (ForallT vs cxt (AppT ListT t))
+    , FunD name [ Clause [] (NormalB $ exp') [] ] ]
diff --git a/src/Language/Haskell/Djinn/HTypes.hs b/src/Language/Haskell/Djinn/HTypes.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/Djinn/HTypes.hs
@@ -0,0 +1,332 @@
+--
+-- Modified to use TemplateHaskell by Claude Heiland-Allen, August 2010
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module Language.Haskell.Djinn.HTypes(HKind(..), HType(..), HSymbol, HEnvironment1, HEnvironment, hTypeToFormula,
+        isHTUnion, getHTVars, substHT,
+        HClause(..), HPat(..), HExpr(..), termToHExpr, termToHClause, getBinderVars) where
+import Language.Haskell.TH (Name, mkName)
+
+import Data.List(union, (\\))
+import Control.Monad(zipWithM)
+import Language.Haskell.Djinn.LJTFormula (Formula(..), Term(..), ConsDesc(..), Symbol(..))
+
+type HSymbol = Name
+
+data HKind
+    = KStar
+    | KArrow HKind HKind
+    | KVar Int
+    deriving (Eq, Show)
+
+data HType
+        = HTApp HType HType
+        | HTVar HSymbol
+        | HTCon HSymbol
+        | HTTuple [HType]
+        | HTArrow HType HType
+        | HTUnion [(HSymbol, [HType])]          -- Only for data types; only at top level
+        deriving (Eq, Show)
+
+type HEnvironment1 = (HSymbol, ([HSymbol], HType))
+type HEnvironment  = [HEnvironment1]
+
+isHTUnion :: HType -> Bool
+isHTUnion (HTUnion _) = True
+isHTUnion _ = False
+
+{-
+htNot :: HSymbol -> HType
+htNot x = HTArrow (HTVar x) (HTCon "Void")
+-}
+
+getHTVars :: HType -> [HSymbol]
+getHTVars (HTApp f a) = getHTVars f `union` getHTVars a
+getHTVars (HTVar v) = [v]
+getHTVars (HTCon _) = []
+getHTVars (HTTuple ts) = foldr union [] (map getHTVars ts)
+getHTVars (HTArrow f a) = getHTVars f `union` getHTVars a
+getHTVars _ = error "getHTVars"
+
+-------------------------------
+
+hTypeToFormula :: HEnvironment -> HType -> Formula
+hTypeToFormula ss (HTTuple ts) = Conj (map (hTypeToFormula ss) ts)
+hTypeToFormula ss (HTArrow t1 t2) = hTypeToFormula ss t1 :-> hTypeToFormula ss t2
+hTypeToFormula ss (HTUnion ctss) = Disj [ (ConsDesc c (length ts), hTypeToFormula ss (HTTuple ts)) | (c, ts) <- ctss ]
+hTypeToFormula ss t = 
+    case expandSyn ss t [] of
+    Nothing -> PVar $ SymbolS $ show t
+    Just t' -> hTypeToFormula ss t'
+
+expandSyn :: HEnvironment -> HType -> [HType] -> Maybe HType
+expandSyn ss (HTApp f a) as = expandSyn ss f (a:as)
+expandSyn ss (HTCon c) as =
+    case lookup c ss of
+    Just (vs, t) | length vs == length as -> Just $ substHT (zip vs as) t
+    _ -> Nothing
+expandSyn _ _ _ = Nothing
+
+substHT :: [(HSymbol, HType)] -> HType -> HType
+substHT r (HTApp f a) = HTApp (substHT r f) (substHT r a)
+substHT r t@(HTVar v) =
+    case lookup v r of
+    Nothing -> t
+    Just t' -> t'
+substHT _ t@(HTCon _) = t
+substHT r (HTTuple ts) = HTTuple (map (substHT r) ts)
+substHT r (HTArrow f a) = HTArrow (substHT r f) (substHT r a)
+substHT r (HTUnion (ctss)) = HTUnion [ (c, map (substHT r) ts) | (c, ts) <- ctss ]
+
+
+-------------------------------
+
+
+data HClause = HClause HSymbol [HPat] HExpr
+    deriving (Show, Eq)
+
+data HPat = HPVar HSymbol | HPCon HSymbol | HPTuple [HPat] | HPAt HSymbol HPat | HPApply HPat HPat
+    deriving (Show, Eq)
+
+data HExpr = HELam [HPat] HExpr | HEApply HExpr HExpr | HECon HSymbol | HEVar HSymbol | HETuple [HExpr] |
+        HECase HExpr [(HPat, HExpr)]
+    deriving (Show, Eq)
+
+unSymbol :: Symbol -> HSymbol
+unSymbol (Symbol  s) =        s
+unSymbol (SymbolS s) = mkName s
+
+termToHExpr :: Term -> HExpr
+termToHExpr term = niceNames $ etaReduce $ remUnusedVars $ fst $ conv [] term
+  where conv _vs (Var s) = (HEVar $ unSymbol s, [])
+        conv vs (Lam s te) = 
+                let hs = unSymbol s
+                    (te', ss) = conv (hs : vs) te
+                in  (hELam [convV hs ss] te', ss)
+        conv vs (Apply (Cinj (ConsDesc s n) _) a) = (f $ foldl HEApply (HECon s) as, ss)
+                where (f, as) = unTuple n ha
+                      (ha, ss) = conv vs a
+        conv vs (Apply te1 te2) = convAp vs te1 [te2]
+--        conv _vs (Ctuple 0) = (HECon "()", [])
+        conv _vs (Ctuple 0) = (HETuple [], [])
+        conv _vs e = error $ "termToHExpr " ++ show e
+
+        unTuple 0 _ = (id, [])
+        unTuple 1 a = (id, [a])
+        unTuple n (HETuple as) | length as == n = (id, as)
+        unTuple n e = error $ "unTuple: unimplemented " ++ show (n, e)
+
+        unTupleP 0 _ = []
+--      unTupleP 1 p = [p]
+        unTupleP n (HPTuple ps) | length ps == n = ps
+        unTupleP n p = error $ "unTupleP: unimplemented " ++ show (n, p)
+
+        convAp vs (Apply te1 te2) as = convAp vs te1 (te2:as)
+        convAp vs (Ctuple n) as | length as == n =
+                let (es, sss) = unzip $ map (conv vs) as
+                in  (hETuple es, concat sss)
+        convAp vs (Ccases cds) (se : es) =
+                let (alts, ass) = unzip $ zipWith cAlt es cds
+                    cAlt (Lam v e) (ConsDesc c n) =
+                        let hv = unSymbol v
+                            (he, ss) = conv (hv : vs) e
+                            ps = case lookup hv ss of
+                                 Nothing -> replicate n underscore
+                                 Just p -> unTupleP n p
+                        in  ((foldl HPApply (HPCon c) ps, he), ss)
+                    cAlt e _ = error $ "cAlt " ++ show e
+                    (e', ess) = conv vs se
+                in  (hECase e' alts, ess ++ concat ass)
+        convAp vs (Csplit n) (b : a : as) =
+                let (hb, sb) = conv vs b
+                    (a', sa) = conv vs a
+                    (as', sss) = unzip $ map (conv vs) as
+                    (ps, b') = unLam n hb
+                    unLam 0 e = ([], e)
+                    unLam k (HELam ps0 e) | length ps0 >= n = let (ps1, ps2) = splitAt k ps0 in (ps1, hELam ps2 e)
+                    unLam k e = error $ "unLam: unimplemented" ++ show (k, e)
+                in  case a' of
+                        HEVar v | v `elem` vs && null as -> (b', [(v, HPTuple ps)] ++ sb ++ sa)
+                        _ -> (foldr HEApply (hECase a' [(HPTuple ps, b')]) as',
+                              sb ++ sa ++ concat sss)
+                    
+        convAp vs f as = 
+                let (es, sss) = unzip $ map (conv vs) (f:as)
+                in  (foldl1 HEApply es, concat sss)
+
+        convV hs ss =
+                case lookup hs ss of
+                Nothing -> HPVar hs
+                Just p -> HPAt hs p
+
+        hETuple [e] = e
+        hETuple es = HETuple es
+
+niceNames :: HExpr -> HExpr
+niceNames e =
+    let bvars = filter (/= mkName "_") $ getBinderVarsHE e
+        chars = ['a'..'z']
+        nvars = map (:[]) chars ++ [ cs ++ [c] | cs <- nvars, c <- chars ]
+        freevars = getAllVars e \\ bvars
+        vars = map mkName nvars \\ freevars
+        sub = zip bvars vars
+    in  hESubst sub e
+
+hELam :: [HPat] -> HExpr -> HExpr
+hELam [] e = e
+hELam ps (HELam ps' e) = HELam (ps ++ ps') e
+hELam ps e = HELam ps e
+
+hECase :: HExpr -> [(HPat, HExpr)] -> HExpr
+--hECase e [] = HEApply (HEVar "void") e
+--hECase _ [(HPCon "()", e)] = e
+hECase e pes | all (uncurry eqPatExpr) pes = e
+hECase e [(p, HELam ps b)] = HELam ps $ hECase e [(p, b)]
+hECase se alts@((_, HELam ops _):_) | m > 0 = HELam (take m ops) $ hECase se alts'
+  where m = minimum (map (numBind . snd) alts)
+        numBind (HELam ps _) = length (takeWhile isPVar ps)
+        numBind _ = 0
+        isPVar (HPVar _) = True
+        isPVar _ = False
+        alts' = [ let (ps1, ps2) = splitAt m ps in (cps, hELam ps2 $ hESubst (zipWith (\ (HPVar v) n -> (v, n)) ps1 ns) e)
+                  | (cps, HELam ps e) <- alts ]
+        ns = [ n | HPVar n <- take m ops ]
+-- if all arms are equal and there are at least two alternatives there can be no bound vars
+-- from the patterns
+hECase _ ((_,e):alts@(_:_)) | all (alphaEq e . snd) alts = e
+hECase e alts = HECase e alts
+
+eqPatExpr :: HPat -> HExpr -> Bool
+eqPatExpr (HPVar s) (HEVar s') = s == s'
+eqPatExpr (HPCon s) (HECon s') = s == s'
+eqPatExpr (HPTuple ps) (HETuple es) = and (zipWith eqPatExpr ps es)
+eqPatExpr (HPApply pf pa) (HEApply ef ea) = eqPatExpr pf ef && eqPatExpr pa ea
+eqPatExpr _ _ = False
+
+alphaEq :: HExpr -> HExpr -> Bool
+alphaEq e1 e2 | e1 == e2 = True
+alphaEq (HELam ps1 e1) (HELam ps2 e2) =
+    Nothing /= do
+        s <- matchPat (HPTuple ps1) (HPTuple ps2)
+        if alphaEq (hESubst s e1) e2 then
+            return ()
+         else
+            Nothing
+alphaEq (HEApply f1 a1) (HEApply f2 a2) = alphaEq f1 f2 && alphaEq a1 a2
+alphaEq (HECon s1) (HECon s2) = s1 == s2
+alphaEq (HEVar s1) (HEVar s2) = s1 == s2
+alphaEq (HETuple es1) (HETuple es2) | length es1 == length es2 = and (zipWith alphaEq es1 es2)
+alphaEq (HECase e1 alts1) (HECase e2 alts2) =
+    alphaEq e1 e2 && and (zipWith alphaEq [ HELam [p] e | (p, e) <- alts1 ] [ HELam [p] e | (p, e) <- alts2 ])
+alphaEq _ _ = False
+
+matchPat :: HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
+matchPat (HPVar s1) (HPVar s2) = return [(s1, s2)]
+matchPat (HPCon s1) (HPCon s2) | s1 == s2 = return []
+matchPat (HPTuple ps1) (HPTuple ps2) | length ps1 == length ps2 = do
+    ss <- zipWithM matchPat ps1 ps2
+    return $ concat ss
+matchPat (HPAt s1 p1) (HPAt s2 p2) = do
+    s <- matchPat p1 p2
+    return $ (s1, s2) : s
+matchPat (HPApply f1 a1) (HPApply f2 a2) = do
+    s1 <- matchPat f1 f2
+    s2 <- matchPat a1 a2
+    return $ s1 ++ s2
+matchPat _ _ = Nothing
+
+hESubst :: [(HSymbol, HSymbol)] -> HExpr -> HExpr
+hESubst s (HELam ps e) = HELam (map (hPSubst s) ps) (hESubst s e)
+hESubst s (HEApply f a) = HEApply (hESubst s f) (hESubst s a)
+hESubst _ e@(HECon _) = e
+hESubst s (HEVar v) = HEVar $ maybe v id $ lookup v s
+hESubst s (HETuple es) = HETuple (map (hESubst s) es)
+hESubst s (HECase e alts) = HECase (hESubst s e) [(hPSubst s p, hESubst s b) | (p, b) <- alts]
+
+hPSubst :: [(HSymbol, HSymbol)] -> HPat -> HPat
+hPSubst s (HPVar v) = HPVar $ maybe v id $ lookup v s
+hPSubst _ p@(HPCon _) = p
+hPSubst s (HPTuple ps) = HPTuple (map (hPSubst s) ps)
+hPSubst s (HPAt v p) = HPAt (maybe v id $ lookup v s) (hPSubst s p)
+hPSubst s (HPApply f a) = HPApply (hPSubst s f) (hPSubst s a)
+
+
+termToHClause :: HSymbol -> Term -> HClause
+termToHClause i term =
+    case termToHExpr term of
+    HELam ps e -> HClause i ps e
+    e -> HClause i [] e
+
+remUnusedVars :: HExpr -> HExpr
+remUnusedVars expr = fst $ remE expr
+  where remE (HELam ps e) =
+            let (e', vs) = remE e
+            in  (HELam (map (remP vs) ps) e', vs)
+        remE (HEApply f a) =
+            let (f', fs) = remE f
+                (a', as) = remE a
+            in  (HEApply f' a', fs ++ as)
+        remE (HETuple es) =
+            let (es', sss) = unzip (map remE es)
+            in  (HETuple es', concat sss)
+        remE (HECase e alts) =
+            let (e', es) = remE e
+                (alts', sss) = unzip [ let (ee', ss) = remE ee in ((remP ss p, ee'), ss) | (p, ee) <- alts ]
+            in  case alts' of
+                [(u, b)] | u == underscore -> (b, concat sss)
+                _ -> (hECase e' alts', es ++ concat sss)
+        remE e@(HECon _) = (e, [])
+        remE e@(HEVar v) = (e, [v])
+        remP vs p@(HPVar v) = if v `elem` vs then p else underscore
+        remP _vs p@(HPCon _) = p
+        remP vs (HPTuple ps) = hPTuple (map (remP vs) ps)
+        remP vs (HPAt v p) = if v `elem` vs then HPAt v (remP vs p) else remP vs p
+        remP vs (HPApply f a) = HPApply (remP vs f) (remP vs a)
+        hPTuple ps | all (== underscore) ps = underscore
+        hPTuple ps = HPTuple ps
+
+underscore :: HPat
+underscore = HPVar (mkName "_")
+
+getBinderVars :: HClause -> [HSymbol]
+getBinderVars (HClause _ pats expr) = concatMap getBinderVarsHP pats ++ getBinderVarsHE expr
+
+getBinderVarsHE :: HExpr -> [HSymbol]
+getBinderVarsHE expr = gbExp expr
+  where gbExp (HELam ps e) = concatMap getBinderVarsHP ps ++ gbExp e
+        gbExp (HEApply f a) = gbExp f ++ gbExp a
+        gbExp (HETuple es) = concatMap gbExp es
+        gbExp (HECase se alts) = gbExp se ++ concatMap (\ (p, e) -> getBinderVarsHP p ++ gbExp e) alts
+        gbExp _ = []
+
+getBinderVarsHP :: HPat -> [HSymbol]
+getBinderVarsHP pat = gbPat pat
+  where gbPat (HPVar s) = [s]
+        gbPat (HPCon _) = []
+        gbPat (HPTuple ps) = concatMap gbPat ps
+        gbPat (HPAt s p) = s : gbPat p
+        gbPat (HPApply f a) = gbPat f ++ gbPat a
+
+getAllVars :: HExpr -> [HSymbol]
+getAllVars expr = gaExp expr
+  where gaExp (HELam _ps e) = gaExp e
+        gaExp (HEApply f a) = gaExp f `union` gaExp a
+        gaExp (HETuple es) = foldr union [] (map gaExp es)
+        gaExp (HECase se alts) = foldr union (gaExp se) (map (\ (_p, e) -> gaExp e) alts)
+        gaExp (HEVar s) = [s]
+        gaExp _ = []
+
+etaReduce :: HExpr -> HExpr
+etaReduce expr = fst $ eta expr
+  where eta (HELam [HPVar v] (HEApply f (HEVar v'))) | v == v' && v `notElem` vs = (f', vs)
+            where (f', vs) = eta f
+        eta (HELam ps e) = (HELam ps e', vs) where (e', vs) = eta e
+        eta (HEApply f a) = (HEApply f' a', fvs++avs) where (f', fvs) = eta f; (a', avs) = eta a
+        eta e@(HECon _) = (e, [])
+        eta e@(HEVar s) = (e, [s])
+        eta (HETuple es) = (HETuple es', concat vss) where (es', vss) = unzip $ map eta es
+        eta (HECase e alts) = (HECase e' alts', vs ++ concat vss) where (e', vs) = eta e
+                                                                        (alts', vss) = unzip $ [ let (a', ss) = eta a in ((p, a'), ss)
+                                                                                                 | (p, a) <- alts ]
diff --git a/src/Language/Haskell/Djinn/LJT.hs b/src/Language/Haskell/Djinn/LJT.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/Djinn/LJT.hs
@@ -0,0 +1,460 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+--
+-- Modified to use Template Haskell by Claude Heiland-Allen, August 2010
+--
+-- Copyright (c) 2005, 2008 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+-- Intuitionistic theorem prover
+-- Written by Roy Dyckhoff, Summer 1991
+-- Modified to use the LWB syntax  Summer 1997
+-- and simplified in various ways...
+--
+-- Translated to Haskell by Lennart Augustsson December 2005
+--
+-- Incorporates the Vorob'ev-Hudelmaier etc calculus (I call it LJT)
+-- See RD's paper in JSL 1992:
+-- "Contraction-free calculi for intuitionistic logic"
+--
+-- Torkel Franzen (at SICS) gave me good ideas about how to write this
+-- properly, taking account of first-argument indexing,
+-- and I learnt a trick or two from Neil Tennant's "Autologic" book.
+
+module Language.Haskell.Djinn.LJT (
+            module Language.Haskell.Djinn.LJTFormula, provable,
+            prove, Proof) where
+
+import Language.Haskell.TH (newName, Q)
+
+import Control.Monad (liftM, liftM2, foldM)
+import Control.Monad.Logic (
+  LogicT, msplit, observeAllT, MonadLogic, MonadTrans(..), MonadPlus(..))
+
+import Data.List (partition)
+import Debug.Trace (trace)
+
+import Language.Haskell.Djinn.LJTFormula (
+  Symbol(..), Formula(..), Term(..), ConsDesc(..), false, applys)
+
+mtrace :: String -> a -> a
+mtrace m x = if debug then trace m x else x
+-- wrap :: (Show a, Show b) => String -> a -> b -> b
+-- wrap fun args ret = mtrace (fun ++ ": " ++ show args) $
+--                     let o = show ret in seq o $
+--                     mtrace (fun ++ " returns: " ++ o) ret
+wrapM :: (Show a, Show b, Monad m) => String -> a -> m b -> m b
+wrapM fun args mret = do
+    () <- mtrace (fun ++ ": " ++ show args) $ return ()
+    ret <- mret
+    () <- mtrace (fun ++ " returns: " ++ show ret) $ return ()
+    return ret
+debug :: Bool
+debug = False
+
+type MoreSolutions = Bool
+
+provable :: Formula -> Q Bool
+provable a = null `fmap` prove False [] a
+
+prove :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> Q [Proof]
+prove more env a = runP $ redtop more env a
+
+redtop :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> P Proof
+redtop more ifs a = do
+    let form = foldr (:->) a (map snd ifs)
+    p <- redant more [] [] [] [] form
+    nf (foldl Apply p (map (Var . fst) ifs))
+
+------------------------------
+-----
+type Proof = Term
+
+subst :: Term -> Symbol -> Term -> P Term
+subst b x term = sub term
+  where sub t@(Var s') = if x == s' then copy [] b else return t
+        sub (Lam s t) = liftM (Lam s) (sub t)
+        sub (Apply t1 t2) = liftM2 Apply (sub t1) (sub t2)
+        sub t = return t
+
+copy :: [(Symbol, Symbol)] -> Term -> P Term
+copy r (Var s) = return $ Var $ maybe s id $ lookup s r
+copy r (Lam s t) = do
+    s' <- newSym "c"
+    liftM (Lam s') $ copy ((s, s'):r) t
+copy r (Apply t1 t2) = liftM2 Apply (copy r t1) (copy r t2)
+copy _r t = return t
+
+------------------------------
+
+applyAtom :: Term -> Term -> Term
+applyAtom f a = Apply f a
+
+curryt :: Int -> Term -> P Term
+curryt n p = do
+  xs <- mapM (\i -> newSym $ "x_" ++ show i) [0 .. n-1]
+  return $ foldr Lam (Apply p (applys (Ctuple n) (map Var xs))) xs
+
+inj :: ConsDesc -> Int -> Term -> P Term
+inj cd i p = do
+  x <- newSym "x"
+  return $ Lam x $ Apply p (Apply (Cinj cd i) (Var x))
+
+applyImp :: Term -> Term -> P Term
+applyImp p q = do
+  x <- newSym "x"
+  y <- newSym "y"
+  return $ Apply p (Apply q (Lam y $ Apply p (Lam x (Var y))))
+
+-- ((c->d)->false) -> ((c->false)->false, d->false)
+-- p : (c->d)->false)
+-- replace p1 and p2 with the components of the pair
+cImpDImpFalse :: Symbol -> Symbol -> Term -> Term -> P Term
+cImpDImpFalse p1 p2 cdf gp = do
+    [cf, x, d, c] <- mapM newSym ["cf", "x", "d", "c"]
+    let p1b = Lam cf $ Apply cdf $ Lam x $ Apply (Ccases []) $ Apply (Var cf) (Var x)
+        p2b = Lam d $ Apply cdf $ Lam c $ Var d
+    subst p1b p1 gp >>= subst p2b p2
+
+------------------------------
+
+-- More simplifications:
+--  split where no variables used can be removed
+--  either with equal RHS can me merged.
+
+-- Compute the normal form
+nf :: Term -> P Term
+nf ee = spine ee []
+  where spine (Apply f a) as = do a' <- nf a; spine f (a' : as)
+        spine (Lam s e) [] = liftM (Lam s) (nf e)
+        spine (Lam s e) (a : as) = do e' <- subst a s e; spine e' as
+        spine (Csplit n) (b : tup : args) | istup && n <= length xs = spine (applys b xs) args
+          where (istup, xs) = getTup tup
+                getTup (Ctuple _) = (True, [])
+                getTup (Apply f a) = let (tf, as) = getTup f in (tf, a:as)
+                getTup _ = (False, [])
+        spine (Ccases []) (e@(Apply (Ccases []) _) : as) = spine e as
+        spine (Ccases cds) (Apply (Cinj _ i) x : as) | length as >= n = spine (Apply (as!!i) x) (drop n as)
+                where n = length cds
+        spine f as = return $ applys f as
+
+
+------------------------------
+----- Our Proof monad, P, a monad transformer with multiple results
+
+newtype PT q a = P{ _unP :: LogicT q a } -- thanks kmc, Cale, #haskell
+  deriving (Functor, Monad, MonadPlus, MonadLogic, MonadTrans)
+type P a = PT Q a
+liftQ :: Q a -> P a
+liftQ = lift
+
+none :: P a
+none = mzero
+
+many :: [a] -> P a
+many = foldr (\x y -> return x `mplus` y) mzero
+
+atMostOne :: P a -> P a
+atMostOne m = do
+  p <- msplit m
+  case p of
+    Nothing    -> mzero
+    Just (a,_) -> return a
+
+runP :: P a -> Q [a]
+runP (P l) = observeAllT l
+
+
+------------------------------
+----- Atomic formulae
+data AtomF = AtomF Term Symbol
+    deriving (Eq)
+instance Show AtomF where
+    show (AtomF p s) = show p ++ ":" ++ show s
+
+type AtomFs = [AtomF]
+
+findAtoms :: Symbol -> AtomFs -> [Term]
+findAtoms s atoms = [ p | AtomF p s' <- atoms, s == s' ]
+
+--removeAtom :: Symbol -> AtomFs -> AtomFs
+--removeAtom s atoms = [ a | a@(AtomF _ s') <- atoms, s /= s' ]
+
+addAtom :: AtomF -> AtomFs -> AtomFs
+addAtom a as = if a `elem` as then as else a : as
+
+------------------------------
+----- Implications of one atom
+
+data AtomImp = AtomImp Symbol Antecedents
+     deriving (Show)
+type AtomImps = [AtomImp]
+
+extract :: AtomImps -> Symbol -> ([Antecedent], AtomImps)
+extract aatomImps@(atomImp@(AtomImp a' bs) : atomImps) a =
+    case compare a a' of
+    GT -> let (rbs, restImps) = extract atomImps a in (rbs, atomImp : restImps)
+    EQ -> (bs, atomImps)
+    LT -> ([], aatomImps)
+extract _ _ = ([], [])
+
+insert :: AtomImps -> AtomImp -> AtomImps
+insert [] ai = [ ai ]
+insert aatomImps@(atomImp@(AtomImp a' bs') : atomImps) ai@(AtomImp a bs) =
+    case compare a a' of
+    GT -> atomImp : insert atomImps ai
+    EQ -> AtomImp a (bs ++ bs') : atomImps
+    LT -> ai : aatomImps
+
+------------------------------
+----- Nested implications, (a -> b) -> c
+
+data NestImp = NestImp Term Formula Formula Formula -- NestImp a b c represents (a :-> b) :-> c
+    deriving (Eq)
+instance Show NestImp where
+    show (NestImp _ a b c) = show $ (a :-> b) :-> c
+
+type NestImps = [NestImp]
+
+addNestImp :: NestImp -> NestImps -> NestImps
+addNestImp n ns = if n `elem` ns then ns else n : ns
+
+------------------------------
+----- Ordering of nested implications
+heuristics :: Bool
+heuristics = True
+
+order :: NestImps -> Formula -> AtomImps -> NestImps
+order nestImps g atomImps =
+    if heuristics then
+        nestImps
+    else
+        let
+            good_for (NestImp _ _ _ (Disj [])) = True
+            good_for (NestImp _ _ _ g') = g == g'
+            nice_for (NestImp _ _ _ (PVar s)) =
+                case extract atomImps s of
+                (bs', _) -> let bs = [ b | A _ b <- bs'] in g `elem` bs || false `elem` bs
+            nice_for _ = False
+            (good, ok) = partition good_for nestImps
+            (nice, bad) = partition nice_for ok
+        in  good ++ nice ++ bad
+
+------------------------------
+----- Generate a new unique variable
+newSym :: String -> P Symbol
+newSym s = Symbol `fmap` liftQ (newName s)
+
+------------------------------
+----- Generate all ways to select one element of a list
+select :: [a] -> P (a, [a])
+select zs = many [ del n zs | n <- [0 .. length zs - 1] ]
+  where del 0 (x:xs) = (x, xs)
+        del n (x:xs) = let (y,ys) = del (n-1) xs in (y, x:ys)
+        del _ _ = error "select"
+
+------------------------------
+-----
+
+data Antecedent = A Term Formula deriving (Show)
+type Antecedents = [Antecedent]
+
+type Goal = Formula
+
+--
+-- This is the main loop of the proof search.
+--
+-- The redant functions reduce antecedents and the redsucc
+-- function reduces the goal (succedent).
+--
+-- The antecedents are kept in four groups: Antecedents, AtomImps, NestImps, AtomFs
+--   Antecedents contains as yet unclassified antecedents; the redant functions
+--     go through them one by one and reduces and classifies them.
+--   AtomImps contains implications of the form (a -> b), where `a' is an atom.
+--     To speed up the processing it is stored as a map from the `a' to all the
+--     formulae it implies.
+--   NestImps contains implications of the form ((b -> c) -> d)
+--   AtomFs contains atomic formulae.
+--
+-- There is also a proof object associated with each antecedent.
+--
+redant :: MoreSolutions -> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
+redant more antes atomImps nestImps atoms goal =
+    wrapM "redant" (antes, atomImps, nestImps, atoms, goal) $
+    case antes of
+    [] -> redsucc goal
+    a:l -> redant1 a l goal
+  where redant0 l g = redant more l atomImps nestImps atoms g
+        redant1 :: Antecedent -> Antecedents -> Goal -> P Proof
+        redant1 a@(A p f) l g =
+            wrapM "redant1" ((a, l), atomImps, nestImps, atoms, g) $
+            if f == g then
+                -- The goal is the antecedent, we're done.
+                -- XXX But we might want more?
+                if more then
+                    return p `mplus` redant1' a l g
+                else
+                    return p
+            else
+                redant1' a l g
+
+        -- Reduce the first antecedent
+        redant1' :: Antecedent -> Antecedents -> Goal -> P Proof
+        redant1' (A p (PVar s)) l g =
+           let af = AtomF p s
+               (bs, restAtomImps) = extract atomImps s
+           in  redant more ([A (Apply f p) b | A f b <- bs] ++ l) restAtomImps nestImps (addAtom af atoms) g
+        redant1' (A p (Conj bs)) l g = do
+           vs <- mapM (const (newSym "v")) bs
+           gp <- redant0 (zipWith (\ v a -> A (Var v) a) vs bs ++ l) g
+           return $ applys (Csplit (length bs)) [foldr Lam gp vs, p]
+        redant1' (A p (Disj ds)) l g = do
+           vs <- mapM (const (newSym "d")) ds
+           ps <- mapM (\ (v, (_, d)) -> redant1 (A (Var v) d) l g) (zip vs ds)
+           if null ds && g == Disj [] then
+               -- We are about to construct `void p : Void', so we shortcut
+               -- it with just `p'.
+               return p
+            else
+               return $ applys (Ccases (map fst ds)) (p : zipWith Lam vs ps)
+        redant1' (A p (a :-> b)) l g = redantimp p a b l g
+
+        redantimp :: Term -> Formula -> Formula -> Antecedents -> Goal -> P Proof
+        redantimp t c d a g =
+            wrapM "redantimp" (c,d,a,g) $
+            redantimp' t c d a g
+
+        -- Reduce an implication antecedent
+        redantimp' :: Term -> Formula -> Formula -> Antecedents -> Goal -> P Proof
+        -- p : PVar s -> b
+        redantimp' p (PVar s) b l g = redantimpatom p s b l g
+        -- p : (c & d) -> b
+        redantimp' p (Conj cs) b l g = do
+            x <- newSym "x"
+            let imp = foldr (:->) b cs
+            gp <- redant1 (A (Var x) imp) l g
+            cry <- curryt (length cs) p
+            subst cry x gp
+        -- p : (c | d) -> b
+        redantimp' p (Disj ds) b l g = do
+            vs <- mapM (const (newSym "d")) ds
+            gp <- redant0 (zipWith (\ v (_, d) -> A (Var v) (d :-> b)) vs ds ++ l) g
+            foldM (\ r (i, v, (cd, _)) -> inj cd i p >>= \nj -> subst nj v r) gp (zip3 [0..] vs ds)
+        -- p : (c -> d) -> b
+        redantimp' p (c :-> d) b l g = redantimpimp p c d b l g
+
+        redantimpimp :: Term -> Formula -> Formula -> Formula -> Antecedents -> Goal -> P Proof
+        redantimpimp f b c d a g =
+            wrapM "redantimpimp" (b,c,d,a,g) $
+            redantimpimp' f b c d a g
+
+        -- Reduce a double implication antecedent
+        redantimpimp' :: Term -> Formula -> Formula -> Formula -> Antecedents -> Goal -> P Proof
+        -- next clause exploits ~(C->D) <=> (~~C & ~D)
+        -- which isn't helpful when D = false
+        redantimpimp' p c d (Disj []) l g | d /= false = do
+            x <- newSym "x"
+            y <- newSym "y"
+            gp <- redantimpimp (Var x) c false false (A (Var y) (d :-> false) : l) g
+            cImpDImpFalse x y p gp
+        -- p : (c -> d) -> b
+        redantimpimp' p c d b l g = redant more l atomImps (addNestImp (NestImp p c d b) nestImps) atoms g
+
+        -- Reduce an atomic implication
+        redantimpatom :: Term -> Symbol -> Formula -> Antecedents -> Goal -> P Proof
+        redantimpatom p s b l g =
+            wrapM "redantimpatom" (s,b,l,g) $
+            redantimpatom' p s b l g
+
+        redantimpatom' :: Term -> Symbol -> Formula -> Antecedents -> Goal -> P Proof
+        redantimpatom' p s b l g =
+          do
+            a <- cutSearch more $ many (findAtoms s atoms)
+            x <- newSym "x"
+            gp <- redant1 (A (Var x) b) l g
+            mtrace "redantimpatom: LLL" $
+             subst (applyAtom p a) x gp
+          `mplus`
+            (mtrace "redantimpatom: RRR" $
+             redant more l (insert atomImps (AtomImp s [A p b])) nestImps atoms g)
+{-
+            let ps = wrap "redantimpatom findAtoms" atoms $ findAtoms s atoms
+            in  if not (null ps) then do
+                    a <- cutSearch more $ many ps
+                    x <- newSym "x"
+                    gp <- redant1 (A (Var x) b) l g
+                    mtrace "redantimpatom: LLL" $
+                     subst (applyAtom p a) x gp
+                else
+                    mtrace "redantimpatom: RRR" $
+                     redant more l (insert atomImps (AtomImp s [A p b])) nestImps atoms g
+-}
+        -- Reduce the goal, with all antecedents already being classified
+        redsucc :: Goal -> P Proof
+        redsucc g =
+            wrapM "redsucc" (g, atomImps, nestImps, atoms) $
+            redsucc' g
+
+        redsucc' :: Goal -> P Proof
+        redsucc' a@(PVar s) =
+            (cutSearch more $ many (findAtoms s atoms))
+          `mplus`
+            -- The posin check is an optimization.  It gets a little slower without the test.
+            (if posin s atomImps nestImps then
+                redsucc_choice a
+            else
+                none)
+        redsucc' (Conj cs) = do
+            ps <- mapM redsucc cs
+            return $ applys (Ctuple (length cs)) ps
+        -- next clause deals with succedent (A v B) by pushing the
+        -- non-determinism into the treatment of implication on the left
+        redsucc' (Disj ds) = do
+            s1 <- newSym "_"
+            let v = PVar s1
+            redant0 [ A (Cinj cd i) $ d :-> v | (i, (cd, d)) <- zip [0..] ds ] v
+        redsucc' (a :-> b) = do
+            s <- newSym "x"
+            p <- redant1 (A (Var s) a) [] b
+            return $ Lam s p
+
+        -- Now we have the hard part; maybe lots of formulae
+        -- of form (C->D)->B  in nestImps to choose from!
+        -- Which one to take first? We user the order heuristic.
+        redsucc_choice :: Goal -> P Proof
+        redsucc_choice g =
+            wrapM "redsucc_choice" g $
+            redsucc_choice' g
+
+        redsucc_choice' :: Goal -> P Proof
+        redsucc_choice' g = do
+            let ordImps = order nestImps g atomImps
+            (NestImp p c d b, restImps) <-
+                mtrace ("redsucc_choice: order=" ++ show ordImps) $
+                select ordImps
+            x <- newSym "x"
+            z <- newSym "z"
+            qz <- redant more [A (Var z) $ d :-> b] atomImps restImps atoms (c :-> d)
+            gp <- redant more [A (Var x) b] atomImps restImps atoms g
+            ai <- applyImp p (Lam z qz)
+            subst ai x gp
+
+posin :: Symbol -> AtomImps -> NestImps -> Bool
+posin g atomImps nestImps = posin1 g atomImps || posin2 g [ (a :-> b) :-> c | NestImp _ a b c <- nestImps ]
+
+posin1 :: Symbol -> AtomImps -> Bool
+posin1 g atomImps = any (\ (AtomImp _ bs) -> posin2 g [ b | A _ b <- bs]) atomImps
+
+posin2 :: Symbol -> [Formula] -> Bool
+posin2 g bs = any (posin3 g) bs
+
+posin3 :: Symbol -> Formula -> Bool
+posin3 g (Disj as) = all (posin3 g) (map snd as)
+posin3 g (Conj as) = any (posin3 g) as
+posin3 g (_ :-> b) = posin3 g b
+posin3 s (PVar s') = s == s'
+
+cutSearch :: MoreSolutions -> P a -> P a
+cutSearch False p = atMostOne p
+cutSearch True p = p
+
+---------------------------
diff --git a/src/Language/Haskell/Djinn/LJTFormula.hs b/src/Language/Haskell/Djinn/LJTFormula.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/Djinn/LJTFormula.hs
@@ -0,0 +1,73 @@
+--
+-- Modified to use TemplateHaskell by Claude Heiland-Allen, August 2010
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module Language.Haskell.Djinn.LJTFormula(Symbol(..), Formula(..), (<->), (&), {- (|:), -} fnot, false, true,
+        ConsDesc(..),
+        Term(..), applys, freeVars
+        ) where
+import Data.List(union, (\\))
+import Language.Haskell.TH (Name)
+
+infixr 2 :->
+infix  2 <->
+--infixl 3 |:
+infixl 4 &
+
+data Symbol = Symbol Name | SymbolS String
+     deriving (Eq, Ord, Show)
+
+data ConsDesc = ConsDesc Name Int     -- name and arity
+     deriving (Eq, Ord, Show)
+
+data Formula
+        = Conj [Formula]
+        | Disj [(ConsDesc, Formula)]
+        | Formula :-> Formula
+        | PVar Symbol
+     deriving (Eq, Ord, Show)
+
+(<->) :: Formula -> Formula -> Formula
+x <-> y = (x:->y) & (y:->x)
+
+(&) :: Formula -> Formula -> Formula
+x & y = Conj [x, y]
+
+{-
+(|:) :: Formula -> Formula -> Formula
+x |: y = Disj [((ConsDesc "Left" 1), x), ((ConsDesc "Right" 1), y)]
+-}
+
+fnot :: Formula -> Formula
+fnot x = x :-> false
+
+false :: Formula
+false = Disj []
+
+true :: Formula
+true = Conj []
+
+------------------------------
+
+data Term
+        = Var Symbol
+        | Lam Symbol Term
+        | Apply Term Term
+        | Ctuple Int
+        | Csplit Int
+        | Cinj ConsDesc Int
+        | Ccases [ConsDesc]
+        | Xsel Int Int Term             --- XXX just temporary by MJ
+    deriving (Eq, Ord, Show)
+
+applys :: Term -> [Term] -> Term
+applys f as = foldl Apply f as
+
+freeVars :: Term -> [Symbol]
+freeVars (Var s) = [s]
+freeVars (Lam s e) = freeVars e \\ [s]
+freeVars (Apply f a) = freeVars f `union` freeVars a
+freeVars (Xsel _ _ e) = freeVars e
+freeVars _ = []