diff --git a/atp-haskell.cabal b/atp-haskell.cabal
--- a/atp-haskell.cabal
+++ b/atp-haskell.cabal
@@ -1,5 +1,5 @@
 Name:             atp-haskell
-Version:          1.7
+Version:          1.8
 Synopsis:         Translation from Ocaml to Haskell of John Harrison's ATP code
 Description:      This package is a liberal translation from OCaml to Haskell of
                   the automated theorem prover written in OCaml in
@@ -22,6 +22,7 @@
 
 Library
   Build-Depends:
+    applicative-extras,
     base >= 4.8 && < 5,
     containers,
     HUnit,
@@ -42,6 +43,7 @@
     Data.Logic.ATP.Equate
     --
     Data.Logic.ATP.Lit
+    Data.Logic.ATP.LitWrapper
     Data.Logic.ATP.Prop
     Data.Logic.ATP.PropExamples
     Data.Logic.ATP.DefCNF
diff --git a/src/Data/Logic/ATP/Apply.hs b/src/Data/Logic/ATP/Apply.hs
--- a/src/Data/Logic/ATP/Apply.hs
+++ b/src/Data/Logic/ATP/Apply.hs
@@ -50,13 +50,15 @@
 -- an 'IsAtom'.
 class (Eq predicate, Ord predicate, Show predicate, IsString predicate, Pretty predicate) => IsPredicate predicate
 
+-- | The result of applying a predicate to some terms is an atomic
+-- formula whose type is an instance of 'HasApply'.
 class (IsAtom atom, IsPredicate (PredOf atom), IsTerm (TermOf atom)) => HasApply atom where
     type PredOf atom
     type TermOf atom
     applyPredicate :: PredOf atom -> [(TermOf atom)] -> atom
-    foldApply' :: (atom -> r) -> (PredOf atom -> [(TermOf atom)] -> r) -> atom -> r
-    overterms :: ((TermOf atom) -> r -> r) -> r -> atom -> r
-    onterms :: ((TermOf atom) -> (TermOf atom)) -> atom -> atom
+    foldApply' :: (atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
+    overterms :: (TermOf atom -> r -> r) -> r -> atom -> r
+    onterms :: (TermOf atom -> TermOf atom) -> atom -> atom
 
 -- | The set of functions in an atom.
 atomFuncs :: (HasApply atom, function ~ FunOf (TermOf atom)) => atom -> Set (function, Arity)
@@ -89,8 +91,9 @@
 ontermsApply f = foldApply (\p ts -> applyPredicate p (map f ts))
 
 -- | Zip two atoms if they are similar
-zipApplys :: (JustApply atom, term ~ TermOf atom, predicate ~ PredOf atom) =>
-                 (predicate -> [(term, term)] -> Maybe r) -> atom -> atom -> Maybe r
+zipApplys :: (JustApply atom1, term ~ TermOf atom1, predicate ~ PredOf atom1,
+              JustApply atom2, term ~ TermOf atom2, predicate ~ PredOf atom2) =>
+             (predicate -> [(term, term)] -> Maybe r) -> atom1 -> atom2 -> Maybe r
 zipApplys f atom1 atom2 =
     foldApply f' atom1
     where
diff --git a/src/Data/Logic/ATP/Equate.hs b/src/Data/Logic/ATP/Equate.hs
--- a/src/Data/Logic/ATP/Equate.hs
+++ b/src/Data/Logic/ATP/Equate.hs
@@ -1,4 +1,4 @@
--- | ATOM with the Equate predicate
+-- | ATOM with a distinguished Equate predicate.
 
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -16,7 +16,6 @@
     ( HasEquate(equate, foldEquate)
     , (.=.)
     , zipEquates
-    , isEquate
     , prettyEquate
     , overtermsEq
     , ontermsEq
@@ -39,22 +38,24 @@
 import Prelude hiding (pred)
 import Text.PrettyPrint.HughesPJClass (maybeParens, Pretty(pPrintPrec), PrettyLevel)
 
--- | Atoms that support equality must have HasEquate instance
+-- | Atoms that support equality must be an instance of HasEquate
 class HasApply atom => HasEquate atom where
     equate :: TermOf atom -> TermOf atom -> atom
+    -- ^ Create an equate predicate
     foldEquate :: (TermOf atom -> TermOf atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
+    -- ^ Analyze whether a predicate is an equate or a regular apply.
 
--- | Build an equality formula from two terms.
+-- | Combine 'equate' and 'atomic' to build a formula from two terms.
 (.=.) :: (IsFormula formula, HasEquate atom, atom ~ AtomOf formula) => TermOf atom -> TermOf atom -> formula
 a .=. b = atomic (equate a b)
 infix 6 .=.
 
 -- | Zip two atoms that support equality
-zipEquates :: HasEquate atom =>
-              (TermOf atom -> TermOf atom ->
-               TermOf atom -> TermOf atom -> Maybe r)
-           -> (PredOf atom -> [(TermOf atom, TermOf atom)] -> Maybe r)
-           -> atom -> atom -> Maybe r
+zipEquates :: (HasEquate atom1, HasEquate atom2, PredOf atom1 ~ PredOf atom2) =>
+              (TermOf atom1 -> TermOf atom1 ->
+               TermOf atom2 -> TermOf atom2 -> Maybe r)
+           -> (PredOf atom1 -> [(TermOf atom1, TermOf atom2)] -> Maybe r)
+           -> atom1 -> atom2 -> Maybe r
 zipEquates eq ap atom1 atom2 =
     foldEquate eq' ap' atom1
     where
@@ -63,32 +64,30 @@
       ap'' p1 ts1 p2 ts2 | p1 == p2 && length ts1 == length ts2 = ap p1 (zip ts1 ts2)
       ap'' _ _ _ _ = Nothing
 
-isEquate :: HasEquate atom => atom -> Bool
-isEquate = foldEquate (\_ _ -> True) (\_ _ -> False)
-
--- | Format the infix equality predicate applied to two terms.
-prettyEquate :: IsTerm term => PrettyLevel -> Rational -> term -> term -> Doc
-prettyEquate l p t1 t2 =
-    maybeParens (p > atomPrec) $ pPrintPrec l atomPrec t1 <> text "=" <> pPrintPrec l atomPrec t2
+-- | Convert between HasEquate atom types.
+convertEquate :: (HasEquate atom1, HasEquate atom2) =>
+                 (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2
+convertEquate cp ct = foldEquate (\t1 t2 -> equate (ct t1) (ct t2)) (\p1 ts1 -> applyPredicate (cp p1) (map ct ts1))
 
--- | Implementation of 'overterms' for 'HasApply' types.
+-- | Implementation of 'overterms' for 'HasEquate' types.
 overtermsEq :: HasEquate atom => ((TermOf atom) -> r -> r) -> r -> atom -> r
 overtermsEq f r0 = foldEquate (\t1 t2 -> f t2 (f t1 r0)) (\_ ts -> foldr f r0 ts)
 
--- | Implementation of 'onterms' for 'HasApply' types.
+-- | Implementation of 'onterms' for 'HasEquate' types.
 ontermsEq :: HasEquate atom => ((TermOf atom) -> (TermOf atom)) -> atom -> atom
 ontermsEq f = foldEquate (\t1 t2 -> equate (f t1) (f t2)) (\p ts -> applyPredicate p (map f ts))
 
--- | Implementation of Show for HasEquate types
+-- | Implementation of Show for 'HasEquate' types
 showApplyAndEquate :: (HasEquate atom, Show (TermOf atom)) => atom -> String
 showApplyAndEquate atom = foldEquate showEquate showApply atom
 
 showEquate :: Show term => term -> term -> String
 showEquate t1 t2 = "(" ++ show t1 ++ ") .=. (" ++ show t2 ++ ")"
 
-convertEquate :: (HasEquate atom1, HasEquate atom2) =>
-                 (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2
-convertEquate cp ct = foldEquate (\t1 t2 -> equate (ct t1) (ct t2)) (\p1 ts1 -> applyPredicate (cp p1) (map ct ts1))
+-- | Format the infix equality predicate applied to two terms.
+prettyEquate :: IsTerm term => PrettyLevel -> Rational -> term -> term -> Doc
+prettyEquate l p t1 t2 =
+    maybeParens (p > atomPrec) $ pPrintPrec l atomPrec t1 <> text "=" <> pPrintPrec l atomPrec t2
 
 precedenceEquate :: HasEquate atom => atom -> Precedence
 precedenceEquate = foldEquate (\_ _ -> eqPrec) (\_ _ -> pAppPrec)
diff --git a/src/Data/Logic/ATP/Lib.hs b/src/Data/Logic/ATP/Lib.hs
--- a/src/Data/Logic/ATP/Lib.hs
+++ b/src/Data/Logic/ATP/Lib.hs
@@ -54,7 +54,7 @@
     , testLib
     ) where
 
-import Control.Applicative (Alternative(empty, (<|>)))
+import Control.Applicative.Error (Failing(..))
 import Control.Concurrent (forkIO, killThread, newEmptyMVar, putMVar, takeMVar, threadDelay)
 import Control.Monad.RWS (evalRWS, runRWS, RWS)
 import Data.Data (Data)
@@ -77,25 +77,7 @@
 
 -- | An error idiom.  Rather like the error monad, but collect all
 -- errors together
-data Failing a = Success a | Failure [ErrorMsg] deriving Show
 type ErrorMsg = String
-
-instance Functor Failing where
-  fmap _ (Failure fs) = Failure fs
-  fmap f (Success a) = Success (f a)
-
-instance Applicative Failing where
-   pure = Success
-   Failure msgs <*> Failure msgs' = Failure (msgs ++ msgs')
-   Success _ <*> Failure msgs' = Failure msgs'
-   Failure msgs' <*> Success _ = Failure msgs'
-   Success f <*> Success x = Success (f x)
-
-instance Alternative Failing where
-  empty                       = Failure []
-  (Success x) <|> _           = Success x
-  _           <|> (Success y) = Success y
-  (Failure x) <|> (Failure y) = Failure (x ++ y)
 
 failing :: ([String] -> b) -> (a -> b) -> Failing a -> b
 failing f _ (Failure errs) = f errs
diff --git a/src/Data/Logic/ATP/LitWrapper.hs b/src/Data/Logic/ATP/LitWrapper.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Logic/ATP/LitWrapper.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE FlexibleContexts, ScopedTypeVariables, TypeFamilies, UndecidableInstances #-}
+module Data.Logic.ATP.LitWrapper
+    ( JL(unJL)
+    ) where
+
+import Data.Logic.ATP.Formulas
+import Data.Logic.ATP.Lit
+import Data.Logic.ATP.Pretty
+
+-- | Wrapper type to make an IsLiteral value that happens to also be
+-- JustLiteral.  The JL constructor is not exported, JL values can be
+-- built using 'convertToLiteral'.
+newtype JL a = JL {unJL :: a}
+
+instance Pretty a => Pretty (JL a) where
+    pPrint (JL x) = pPrint x
+
+instance HasFixity a => HasFixity (JL a) where
+    precedence = precedence . unJL
+    associativity = associativity . unJL
+
+instance IsLiteral a => IsFormula (JL a) where
+    type AtomOf (JL a) = AtomOf a
+    asBool (JL x) = asBool x
+    true = JL (true :: a)
+    false = JL (false :: a)
+    atomic = JL . atomic
+    overatoms f (JL x) r0 = overatomsLiteral' {-(\y r -> f (JL y) r)-} f x r0
+    onatoms f (JL x) = JL (onatoms f x)
+
+instance (IsFormula (JL a), IsLiteral a) => JustLiteral (JL a)
+
+instance (IsFormula (JL a), IsLiteral a) => IsLiteral (JL a) where
+    naiveNegate (JL x) = JL (naiveNegate x)
+    foldNegation n i (JL x) = foldNegation (n . JL) (i . JL) x
+    foldLiteral' ho ne tf at (JL x) = foldLiteral' (ho . JL) (ne . JL) tf at x
+
+-- | Unsafe local version of overatomsLiteral - assumes lit is a JustLiteral.
+overatomsLiteral' :: IsLiteral lit => (AtomOf lit -> r -> r) -> lit -> r -> r
+overatomsLiteral' f fm r0 =
+        foldLiteral' undefined ne (const r0) (flip f r0) fm
+        where
+          ne fm' = overatomsLiteral' f fm' r0
diff --git a/src/Data/Logic/ATP/Meson.hs b/src/Data/Logic/ATP/Meson.hs
--- a/src/Data/Logic/ATP/Meson.hs
+++ b/src/Data/Logic/ATP/Meson.hs
@@ -176,7 +176,7 @@
 -- -------------------------------------------------------------------------
 
 mexpand1 :: (JustLiteral lit, Ord lit,
-             HasApply atom, IsTerm term, Unify atom v term,
+             HasApply atom, IsTerm term, Unify atom atom,
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
            Set (PrologRule lit)
         -> Set lit
@@ -206,7 +206,7 @@
 -- -------------------------------------------------------------------------
 
 puremeson1 :: forall fof atom term v function.
-              (IsFirstOrder fof, Unify atom v term, Ord fof,
+              (IsFirstOrder fof, Unify atom atom, Ord fof,
                atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
                v ~ VarOf fof, v ~ TVarOf term) =>
               Maybe Depth -> fof -> Failing Depth
@@ -219,7 +219,7 @@
       (cls :: Set (Set (LFormula atom))) = simpcnf id (specialize id (pnf fm) :: PFormula atom)
 
 meson1 :: forall m fof atom predicate term function v.
-          (IsFirstOrder fof, Unify atom (VarOf fof) (TermOf (atom)), Ord fof, HasSkolem function, Monad m,
+          (IsFirstOrder fof, Unify atom atom, Ord fof, HasSkolem function, Monad m,
            atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
           Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
 meson1 maxdl fm =
@@ -230,7 +230,7 @@
 -- With repetition checking and divide-and-conquer search.
 -- -------------------------------------------------------------------------
 
-equal :: (JustLiteral lit, HasApply atom, Unify atom v term, IsTerm term,
+equal :: (JustLiteral lit, HasApply atom, Unify atom atom, IsTerm term,
           atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
          Map v term -> lit -> lit -> Bool
 equal env fm1 fm2 =
@@ -257,7 +257,7 @@
                                    (e1,n2+r1,k1))
                  (env,n1,k)
 
-mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify atom v term,
+mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify atom atom,
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
            Set (PrologRule lit)
         -> Set lit
@@ -284,7 +284,7 @@
             mexpand2' = mexpands rules (Set.insert g ancestors) asm cont
             (Prolog asm c, k') = renamerule k rule
 
-mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom v term, IsTerm term,
+mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term,
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
             Set (PrologRule lit)
          -> Set lit
@@ -317,7 +317,7 @@
 puremeson2 :: forall fof atom term v.
              (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term,
               IsFirstOrder fof,
-              Unify atom v term, Ord fof
+              Unify atom atom, Ord fof
              ) => Maybe Depth -> fof -> Failing Depth
 puremeson2 maxdl fm =
     snd <$> deepen f (Depth 0) maxdl
@@ -328,7 +328,7 @@
       (cls :: Set (Set (LFormula atom))) = simpcnf id (specialize id (pnf fm) :: PFormula atom)
 
 meson2 :: forall m fof atom term function v.
-          (IsFirstOrder fof, Unify atom v term, Ord fof,
+          (IsFirstOrder fof, Unify atom atom, Ord fof,
            HasSkolem function, Monad m,
            atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
           Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
@@ -336,7 +336,7 @@
     askolemize ((.~.)(generalize fm)) >>=
     return . Set.map (puremeson2 maxdl . list_conj) . (simpdnf' :: fof -> Set (Set fof))
 
-meson :: (IsFirstOrder fof, Unify atom v term, HasSkolem function, Monad m, Ord fof,
+meson :: (IsFirstOrder fof, Unify atom atom, HasSkolem function, Monad m, Ord fof,
           atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
          Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
 meson = meson2
diff --git a/src/Data/Logic/ATP/Prop.hs b/src/Data/Logic/ATP/Prop.hs
--- a/src/Data/Logic/ATP/Prop.hs
+++ b/src/Data/Logic/ATP/Prop.hs
@@ -18,10 +18,10 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 module Data.Logic.ATP.Prop
-    ( -- * binary operations
-      BinOp(..), binop
+    (
     -- * Propositional formulas
-    , IsPropositional((.|.), (.&.), (.<=>.), (.=>.), foldPropositional', foldCombination)
+      IsPropositional((.|.), (.&.), (.<=>.), (.=>.), foldPropositional', foldCombination)
+    , BinOp(..), binop
     , (⇒), (==>), (⊃), (→)
     , (⇔), (<=>), (↔), (<==>)
     , (∧), (·)
@@ -103,49 +103,6 @@
 import Text.PrettyPrint.HughesPJClass (maybeParens, PrettyLevel, vcat)
 import Test.HUnit
 
--- | Implication synonyms.  Note that if the -XUnicodeSyntax option is
--- turned on the operator ⇒ can not be declared/used as a function -
--- it becomes a reserved special character used in type signatures.
-(⇒), (⊃), (==>), (→) :: IsPropositional formula => formula -> formula -> formula
-(⇒) = (.=>.)
-(⊃) = (.=>.)
-(==>) = (.=>.)
-(→) = (.=>.)
-infixr 3 .=>., ⇒, ⊃, ==>, →
-
--- | If-and-only-if synonyms
-(<=>), (<==>), (⇔), (↔) :: IsPropositional formula => formula -> formula -> formula
-(<=>) = (.<=>.)
-(<==>) = (.<=>.)
-(⇔) = (.<=>.)
-(↔) = (.<=>.)
-infixl 2 .<=>., <=>, <==>, ⇔, ↔
-
--- | And/conjunction synonyms
-(∧), (·) :: IsPropositional formula => formula -> formula -> formula
-(∧) = (.&.)
-(·) = (.&.)
-infixl 5 .&., ∧, ·
-
--- | Or/disjunction synonyms
-(∨) :: IsPropositional formula => formula -> formula -> formula
-(∨) = (.|.)
-infixl 4 .|., ∨
-
-data BinOp
-    = (:<=>:)
-    | (:=>:)
-    | (:&:)
-    | (:|:)
-    deriving (Eq, Ord, Data, Typeable, Show, Enum, Bounded)
-
--- | Combine formulas with a 'BinOp'.
-binop :: IsPropositional formula => formula -> BinOp -> formula -> formula
-binop f1 (:<=>:) f2 = f1 .<=>. f2
-binop f1 (:=>:) f2 = f1 .=>. f2
-binop f1 (:&:) f2 = f1 .&. f2
-binop f1 (:|:) f2 = f1 .|. f2
-
 -- |A type class for propositional logic.  If the type we are writing
 -- an instance for is a zero-order (aka propositional) logic type
 -- there will generally by a type or a type parameter corresponding to
@@ -183,6 +140,35 @@
                     -> (formula -> formula -> r) -- equivalence
                     -> formula -> r
 
+-- | Implication synonyms.  Note that if the -XUnicodeSyntax option is
+-- turned on the operator ⇒ can not be declared/used as a function -
+-- it becomes a reserved special character used in type signatures.
+(⇒), (⊃), (==>), (→) :: IsPropositional formula => formula -> formula -> formula
+(⇒) = (.=>.)
+(⊃) = (.=>.)
+(==>) = (.=>.)
+(→) = (.=>.)
+infixr 3 .=>., ⇒, ⊃, ==>, →
+
+-- | If-and-only-if synonyms
+(<=>), (<==>), (⇔), (↔) :: IsPropositional formula => formula -> formula -> formula
+(<=>) = (.<=>.)
+(<==>) = (.<=>.)
+(⇔) = (.<=>.)
+(↔) = (.<=>.)
+infixl 2 .<=>., <=>, <==>, ⇔, ↔
+
+-- | And/conjunction synonyms
+(∧), (·) :: IsPropositional formula => formula -> formula -> formula
+(∧) = (.&.)
+(·) = (.&.)
+infixl 5 .&., ∧, ·
+
+-- | Or/disjunction synonyms
+(∨) :: IsPropositional formula => formula -> formula -> formula
+(∨) = (.|.)
+infixl 4 .|., ∨
+
 -- | Deconstruct a 'JustPropositional' formula.
 foldPropositional :: JustPropositional pf =>
                      (pf -> BinOp -> pf -> r) -- ^ fold on a binary operation formula
@@ -191,6 +177,22 @@
                   -> (AtomOf pf -> r)         -- ^ fold on an atomic formula
                   -> pf -> r
 foldPropositional = foldPropositional' (error "JustPropositional failure")
+
+-- | This type is used to construct the first argument of 'foldPropositional'.
+data BinOp
+    = (:<=>:)
+    | (:=>:)
+    | (:&:)
+    | (:|:)
+    deriving (Eq, Ord, Data, Typeable, Show, Enum, Bounded)
+
+-- | Combine formulas with a 'BinOp', for use building the first
+-- argument of 'foldPropositional'.
+binop :: IsPropositional formula => formula -> BinOp -> formula -> formula
+binop f1 (:<=>:) f2 = f1 .<=>. f2
+binop f1 (:=>:) f2 = f1 .=>. f2
+binop f1 (:&:) f2 = f1 .&. f2
+binop f1 (:|:) f2 = f1 .|. f2
 
 -- | Combine two 'JustPropositional' formulas if they are similar.
 zipPropositional :: (JustPropositional pf1, JustPropositional pf2) =>
diff --git a/src/Data/Logic/ATP/Resolution.hs b/src/Data/Logic/ATP/Resolution.hs
--- a/src/Data/Logic/ATP/Resolution.hs
+++ b/src/Data/Logic/ATP/Resolution.hs
@@ -68,7 +68,7 @@
 
 -- | MGU of a set of literals.
 mgu :: forall lit atom term v.
-       (IsLiteral lit, HasApply atom, Unify atom v term, IsTerm term,
+       (JustLiteral lit, HasApply atom, Unify atom atom, IsTerm term,
         atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
        Set lit -> StateT (Map v term) Failing (Map v term)
 mgu l =
@@ -79,7 +79,7 @@
             _ -> solve <$> get
       _ -> solve <$> get
 
-unifiable :: (IsLiteral lit, IsTerm term, HasApply atom, Unify atom v term,
+unifiable :: (JustLiteral lit, IsTerm term, HasApply atom, Unify atom atom,
               atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
              lit -> lit -> Bool
 unifiable p q = failing (const False) (const True) (execStateT (unify_literals p q) Map.empty)
@@ -100,7 +100,7 @@
 -- General resolution rule, incorporating factoring as in Robinson's paper.
 -- -------------------------------------------------------------------------
 
-resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom v term, IsTerm term,
+resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term,
                atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
               Set lit -> Set lit -> lit -> Set lit -> Set lit
 resolvents cl1 cl2 p acc =
@@ -117,7 +117,7 @@
       -- ps2 :: Set fof
       ps2 = Set.filter (unifiable ((.~.) p)) cl2
 
-resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom v term, IsTerm term,
+resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term,
                     atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
                    Set lit -> Set lit -> Set lit
 resolve_clauses cls1 cls2 =
@@ -129,7 +129,7 @@
 -- Basic "Argonne" loop.
 -- -------------------------------------------------------------------------
 
-resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify atom v term,
+resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify atom atom,
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
             Set (Set lit) -> Set (Set lit) -> Failing Bool
 resloop1 used unused =
@@ -145,13 +145,13 @@
 pure_resolution1 :: forall fof atom term v.
                     (atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term,
                      IsFirstOrder fof,
-                     Unify atom v term,
+                     Unify atom atom,
                      Ord fof, Pretty fof
                     ) => fof -> Failing Bool
 pure_resolution1 fm = resloop1 Set.empty (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom)))
 
 resolution1 :: forall m fof atom term v function.
-               (IsFirstOrder fof, Unify atom v term, Ord fof, HasSkolem function, Monad m,
+               (IsFirstOrder fof, Unify atom atom, Ord fof, HasSkolem function, Monad m,
                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) =>
                fof -> SkolemT m function (Set (Failing Bool))
 resolution1 fm = askolemize ((.~.)(generalize fm)) >>= return . Set.map (pure_resolution1 . list_conj) . (simpdnf' :: fof -> Set (Set fof))
@@ -220,7 +220,7 @@
 
 -- | With deletion of tautologies and bi-subsumption with "unused".
 resolution2 :: forall fof atom term v function m.
-               (IsFirstOrder fof, Unify atom v term, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,
+               (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,
                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) =>
                fof -> SkolemT m function (Set (Failing Bool))
 resolution2 fm = askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_resolution2 . list_conj) . (simpdnf' :: fof -> Set (Set fof))
@@ -228,13 +228,13 @@
 pure_resolution2 :: forall fof atom term v.
                     (IsFirstOrder fof, Ord fof, Pretty fof,
                      HasApply atom, IsTerm term,
-                     Unify atom v term, Match (atom, atom) v term,
+                     Unify atom atom, Match (atom, atom) v term,
                      atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term) =>
                     fof -> Failing Bool
 pure_resolution2 fm = resloop2 Set.empty (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom)))
 
 resloop2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
-             Unify atom v term, Match (atom, atom) v term,
+             Unify atom atom, Match (atom, atom) v term,
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
             Set (Set lit) -> Set (Set lit) -> Failing Bool
 resloop2 used unused =
@@ -295,20 +295,20 @@
 
 -- | Positive (P1) resolution.
 presolution :: forall fof atom term v function m.
-               (IsFirstOrder fof, Unify atom v term, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof,
+               (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof,
                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
                fof -> SkolemT m function (Set (Failing Bool))
 presolution fm =
     askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_presolution . list_conj) . (simpdnf' :: fof -> Set (Set fof))
 
 pure_presolution :: forall fof atom term v.
-                    (IsFirstOrder fof, Unify atom v term, Match (atom, atom) v term, Ord fof, Pretty fof,
+                    (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, Ord fof, Pretty fof,
                      atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term) =>
                     fof -> Failing Bool
 pure_presolution fm = presloop Set.empty (simpcnf id (specialize id (pnf fm :: fof) ::  PFormula atom) :: Set (Set (LFormula atom)))
 
 presloop :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
-             Match (atom, atom) v term, Unify atom v term,
+             Match (atom, atom) v term, Unify atom atom,
              atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
             Set (Set lit) -> Set (Set lit) -> Failing Bool
 presloop used unused =
@@ -323,7 +323,7 @@
           then Success True
           else presloop used' (Set.fold (incorporate cl) ros news)
 
-presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify atom v term,
+presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify atom atom,
                      atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
                     Set lit -> Set lit -> Set lit
 presolve_clauses cls1 cls2 =
@@ -333,7 +333,7 @@
 
 -- | Introduce a set-of-support restriction.
 resolution3 :: forall fof atom term v function m.
-               (IsFirstOrder fof, Unify atom v term, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,
+               (IsFirstOrder fof, Unify atom atom, Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof,
                 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
                fof -> SkolemT m function (Set (Failing Bool))
 resolution3 fm =
@@ -342,7 +342,7 @@
 pure_resolution3 :: forall fof atom term v.
                     (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term,
                      IsFirstOrder fof,
-                     Unify atom v term,
+                     Unify atom atom,
                      Match (atom, atom) v term,
                      Ord fof, Pretty fof) => fof -> Failing Bool
 pure_resolution3 fm =
diff --git a/src/Data/Logic/ATP/Tableaux.hs b/src/Data/Logic/ATP/Tableaux.hs
--- a/src/Data/Logic/ATP/Tableaux.hs
+++ b/src/Data/Logic/ATP/Tableaux.hs
@@ -30,7 +30,8 @@
 import Data.Logic.ATP.Formulas (atomic, IsFormula(asBool, AtomOf), onatoms, overatoms)
 import Data.Logic.ATP.Herbrand (davisputnam)
 import Data.Logic.ATP.Lib ((|=>), allpairs, deepen, Depth(Depth), distrib, evalRS, Failing(Success, Failure), failing, settryfind, tryfindM)
-import Data.Logic.ATP.Lit ((.~.), IsLiteral, JustLiteral, LFormula, positive)
+import Data.Logic.ATP.Lit ((.~.), convertToLiteral, IsLiteral, JustLiteral, LFormula, positive)
+import Data.Logic.ATP.LitWrapper (JL)
 import Data.Logic.ATP.Pretty (assertEqual', Pretty(pPrint), prettyShow, text)
 import Data.Logic.ATP.Prop ( (.&.), (.=>.), (.<=>.), (.|.), BinOp((:&:), (:|:)), PFormula, simpdnf)
 import Data.Logic.ATP.Quantified (exists, foldQuantified, for_all, Quant((:!:)))
@@ -44,13 +45,13 @@
 import Test.HUnit hiding (State)
 
 -- | Unify complementary literals.
-unify_complements :: (IsLiteral lit, HasApply atom, Unify atom v term,
-                      atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
-                     lit -> lit -> StateT (Map v term) Failing ()
+unify_complements :: (IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2, Unify atom1 atom2,
+                      atom1 ~ AtomOf lit1, atom2 ~ AtomOf lit2, term ~ TermOf atom1, term ~ TermOf atom2, v ~ TVarOf term) =>
+                     lit1 -> lit2 -> StateT (Map v term) Failing ()
 unify_complements p q = unify_literals p ((.~.) q)
 
 -- | Unify and refute a set of disjuncts.
-unify_refute :: (IsLiteral lit, Ord lit, HasApply atom, Unify atom v term, IsTerm term,
+unify_refute :: (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom, IsTerm term,
                  atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
                 Set (Set lit) -> Map v term -> Failing (Map v term)
 unify_refute djs env =
@@ -64,7 +65,7 @@
 
 -- | Hence a Prawitz-like procedure (using unification on DNF).
 prawitz_loop :: forall lit atom v term.
-                (JustLiteral lit, Ord lit, HasApply atom, Unify atom v term,
+                (JustLiteral lit, Ord lit, HasApply atom, Unify atom atom,
                  atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
                 Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
 prawitz_loop djs0 fvs djs n =
@@ -77,7 +78,7 @@
       newvar k = vt (fromString ("_" ++ show (n * length fvs + k)))
 
 prawitz :: forall formula atom term function v.
-           (IsFirstOrder formula, Ord formula, Unify atom v term, HasSkolem function, Show formula,
+           (IsFirstOrder formula, Ord formula, Unify atom atom, HasSkolem function, Show formula,
             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
             v ~ TVarOf term, v ~ SVarOf function) =>
            formula -> Int
@@ -106,7 +107,7 @@
 -- Comparison of number of ground instances.
 -- -------------------------------------------------------------------------
 
-compare :: (IsFirstOrder formula, Ord formula, Unify atom v term, HasSkolem function, Show formula,
+compare :: (IsFirstOrder formula, Ord formula, Unify atom atom, HasSkolem function, Show formula,
             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
             v ~ TVarOf term, v ~ SVarOf function) =>
            formula -> (Int, Int)
@@ -174,13 +175,13 @@
 
 -- | More standard tableau procedure, effectively doing DNF incrementally.  (p. 177)
 tableau :: forall formula atom term v function.
-           (IsFirstOrder formula, Unify atom v term,
+           (IsFirstOrder formula, Unify atom atom,
             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) =>
            [formula] -> Depth -> RWS () () () (Failing (K, Map v term))
 tableau fms n0 =
     go (fms, [], n0) (return . Success) (K 0, Map.empty)
     where
-      go :: ([formula], [formula], Depth)
+      go :: ([formula], [JL formula], Depth)
          -> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
          -> (K, Map v term)
          -> RWS () () () (Failing (K, Map v term))
@@ -203,20 +204,21 @@
 
             go2 :: formula -> [formula] -> RWS () () () (Failing (K, Map v term))
             go2 fm' unexp' =
-                tryfindM (tryLit fm') lits >>=
-                failing (\_ -> go (unexp', fm' : lits, n) cont (k, env))
+                let (fm'' :: JL formula) = convertToLiteral (error "expected JustLiteral") id fm' in
+                tryfindM (tryLit fm'') lits >>=
+                failing (\_ -> go (unexp', fm'' : lits, n) cont (k, env))
                         (return . Success)
-            tryLit :: formula -> formula -> RWS () () () (Failing (K, Map v term))
+            tryLit :: JL formula -> JL formula -> RWS () () () (Failing (K, Map v term))
             tryLit fm' l = failing (return . Failure) (\env' -> cont (k, env')) (execStateT (unify_complements fm' l) env)
 
-tabrefute :: (IsFirstOrder formula, Unify atom v term,
+tabrefute :: (IsFirstOrder formula, Unify atom atom,
               atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) =>
              Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
 tabrefute limit fms =
     let r = deepen (\n -> (,n) <$> evalRS (tableau fms n) () ()) (Depth 0) limit in
     failing Failure (Success . fst) r
 
-tab :: (IsFirstOrder formula, Unify atom v term, Pretty formula, HasSkolem function,
+tab :: (IsFirstOrder formula, Unify atom atom, Pretty formula, HasSkolem function,
         atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
         v ~ TVarOf term, v ~ SVarOf function) =>
        Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
@@ -283,7 +285,7 @@
 -- Try to split up the initial formula first; often a big improvement.
 -- -------------------------------------------------------------------------
 splittab :: forall formula atom term v function.
-            (IsFirstOrder formula, Unify atom v term, Ord formula, Pretty formula, HasSkolem function,
+            (IsFirstOrder formula, Unify atom atom, Ord formula, Pretty formula, HasSkolem function,
              atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
              v ~ TVarOf term, v ~ SVarOf function) =>
             formula -> [Failing ((K, Map v term), Depth)]
diff --git a/src/Data/Logic/ATP/Term.hs b/src/Data/Logic/ATP/Term.hs
--- a/src/Data/Logic/ATP/Term.hs
+++ b/src/Data/Logic/ATP/Term.hs
@@ -1,3 +1,8 @@
+-- | A Term is a expression representing a domain element.  It is
+-- composed of variables which can be bound to domain elements, or
+-- functions which can be applied to terms to yield other domain
+-- elements.
+
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
diff --git a/src/Data/Logic/ATP/Unif.hs b/src/Data/Logic/ATP/Unif.hs
--- a/src/Data/Logic/ATP/Unif.hs
+++ b/src/Data/Logic/ATP/Unif.hs
@@ -24,36 +24,38 @@
 import Control.Monad.State -- (evalStateT, runStateT, State, StateT, get)
 import Data.Bool (bool)
 import Data.List as List (map)
-import Data.Logic.ATP.Apply (HasApply(TermOf), JustApply, zipApplys)
+import Data.Logic.ATP.Apply (HasApply(TermOf, PredOf), JustApply, zipApplys)
 import Data.Logic.ATP.Equate (HasEquate, zipEquates)
 import Data.Logic.ATP.FOL (tsubst)
 import Data.Logic.ATP.Formulas (IsFormula(AtomOf))
 import Data.Logic.ATP.Lib (Failing(Success, Failure))
-import Data.Logic.ATP.Lit (IsLiteral, zipLiterals')
+import Data.Logic.ATP.Lit (IsLiteral, JustLiteral, zipLiterals')
 import Data.Logic.ATP.Skolem (SkAtom, SkTerm)
-import Data.Logic.ATP.Term (IsTerm(..), V)
+import Data.Logic.ATP.Term (IsTerm(..))
 import Data.Map.Strict as Map
 import Data.Maybe (fromMaybe)
-import Data.Sequence (Seq, viewl, ViewL(EmptyL, (:<)))
+-- import Data.Sequence (Seq, viewl, ViewL(EmptyL, (:<)))
 import Test.HUnit hiding (State)
 
 -- | Main unification procedure.
-class Unify a v term where
-    unify :: a -> a -> StateT (Map v term) Failing ()
+class TermOf a ~ TermOf b => Unify a b where
+    unify :: a -> b -> StateT (Map (TVarOf (TermOf a)) (TermOf a)) Failing ()
     -- ^ Unify the two elements of a pair, collecting variable
     -- assignments in the state.
 
-instance Unify a v term => Unify [a] v term where
+{-
+instance Unify a b => Unify [a] [b] where
     unify [] [] = return ()
     unify (x : xs) (y : ys) = unify x y >> unify xs ys
     unify _ _ = fail "unify - list length mismatch"
 
-instance Unify a v term => Unify (Seq a) v term where
+instance Unify a b => Unify (Seq a) (Seq b) where
     unify xs ys =
         case (viewl xs, viewl ys) of
           (EmptyL, EmptyL) -> return ()
           (x :< xs', y :< ys') -> unify x y >> unify xs' ys'
           _ -> fail "unify - Seq list length mismatch"
+-}
 
 unify_terms :: (IsTerm term, v ~ TVarOf term) => [(term,term)] -> StateT (Map v term) Failing ()
 unify_terms = mapM_ (uncurry unify_term_pair)
@@ -103,10 +105,14 @@
 unify_and_apply eqs =
     fullunify eqs >>= \i -> return $ List.map (\ (t1, t2) -> (tsubst i t1, tsubst i t2)) eqs
 
--- | Unify literals
-unify_literals :: (IsLiteral lit, HasApply atom, Unify atom v term,
-                   atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
-                  lit -> lit -> StateT (Map v term) Failing ()
+-- | Unify literals, perhaps of different types, but sharing term and
+-- variable type.  Note that only one needs to be 'JustLiteral', if
+-- the unification succeeds the other must have been too, if it fails,
+-- who cares.
+unify_literals :: (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1,
+                   JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2,
+                   Unify atom1 atom2, v ~ TVarOf term) =>
+                  lit1 -> lit2 -> StateT (Map v term) Failing ()
 unify_literals f1 f2 =
     fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2)
     where
@@ -115,13 +121,17 @@
       tf p q = if p == q then Just (unify_terms []) else Nothing
       at a1 a2 = Just (unify a1 a2)
 
-unify_atoms :: (JustApply atom, term ~ TermOf atom, v ~ TVarOf term) =>
-               (atom, atom) -> StateT (Map v term) Failing ()
+unify_atoms :: (JustApply atom1, term ~ TermOf atom1,
+                JustApply atom2, term ~ TermOf atom2,
+                v ~ TVarOf term, PredOf atom1 ~ PredOf atom2) =>
+               (atom1, atom2) -> StateT (Map v term) Failing ()
 unify_atoms (a1, a2) =
     maybe (fail "unify_atoms") id (zipApplys (\_ tpairs -> Just (unify_terms tpairs)) a1 a2)
 
-unify_atoms_eq :: (HasEquate atom, term ~ TermOf atom, v ~ TVarOf term) =>
-                  atom -> atom -> StateT (Map v term) Failing ()
+unify_atoms_eq :: (HasEquate atom1, term ~ TermOf atom1,
+                   HasEquate atom2, term ~ TermOf atom2,
+                   PredOf atom1 ~ PredOf atom2, v ~ TVarOf term) =>
+                  atom1 -> atom2 -> StateT (Map v term) Failing ()
 unify_atoms_eq a1 a2 =
     maybe (fail "unify_atoms") id (zipEquates (\l1 r1 l2 r2 -> Just (unify_terms [(l1, l2), (r1, r2)]))
                                               (\_ tpairs -> Just (unify_terms tpairs))
@@ -133,7 +143,7 @@
 --        where
 --          app (t1, t2) = fullunify eqs >>= \i -> return $ (tsubst i t1, tsubst i t2)
 
-instance Unify SkAtom V SkTerm where
+instance Unify SkAtom SkAtom where
     unify = unify_atoms_eq
 
 test01, test02, test03, test04 :: Test