diff --git a/FMCt.cabal b/FMCt.cabal
index 6e165de..0462787 100644
--- a/FMCt.cabal
+++ b/FMCt.cabal
@@ -39,6 +39,7 @@ common library-specs
     FMCt.Syntax
     FMCt.TypeChecker
     FMCt.TypeChecker2
+    FMCt.TypeCheckerAlt
     FMCt.Aux.Pretty
     FMCt.Aux.ToTex
 
diff --git a/src/FMCt.hs b/src/FMCt.hs
index e20aca6..d04278a 100644
--- a/src/FMCt.hs
+++ b/src/FMCt.hs
@@ -1,11 +1,13 @@
 -- | Module is made just for Re-Exporting basic functions.
-module FMCt (module X, module XX) where
+module FMCt (module X, module XX, module Y) where
 
-import FMCt.Aux.Pretty   as X
-import FMCt.Aux.ToTex    as X
-import FMCt.Evaluator    as X (eval, eval1, eval1', evalToString)
-import FMCt.Examples     as X (examplesList)
-import FMCt.Parsing      as X (parseFMC, parseFMCtoString, parseType)
-import FMCt.Pretty       as X (printOutput, printStack)
-import FMCt.TypeChecker  as X (derive, typeCheck, typeCheckP)
-import FMCt.TypeChecker2 as XX (derive2, getTermType, pShow')
+import FMCt.Aux.Pretty     as X
+import FMCt.Aux.ToTex      as X
+import FMCt.Evaluator      as X  (eval, eval1, eval1', evalToString)
+import FMCt.Examples       as X  (examplesList)
+import FMCt.Parsing        as X  (parseFMC, parseFMCtoString, parseType)
+import FMCt.Pretty         as X  (printOutput, printStack)
+import FMCt.TypeChecker    as X  (derive, typeCheck, typeCheckP)
+import FMCt.TypeChecker2   as XX (derive2, getTermType, pShow', normalForm, testD2)
+import FMCt.Syntax         as X  (T, Type(..),)
+import FMCt.TypeCheckerAlt as Y  (derive1, testD1)
diff --git a/src/FMCt/Aux/TC.hs b/src/FMCt/Aux/TC.hs
new file mode 100644
index 0000000..7887c56
--- /dev/null
+++ b/src/FMCt/Aux/TC.hs
@@ -0,0 +1,112 @@
+module FMCt.Aux.TC where
+
+import FMCt.Syntax
+import Text.Read (readMaybe)
+
+-- | Merge contexts
+mergeCtx :: Context -> Context -> Either TError Context
+mergeCtx ox oy = makeSet ox oy
+  where
+    makeSet [] x = pure x
+    makeSet (t : xs) [] = (t :) <$> makeSet xs oy
+    makeSet t@((term, ty) : xs) ((term', ty') : ys) =
+        if term /= term'
+            then makeSet t ys
+            else
+                if ty == ty'
+                    then makeSet xs oy
+                    else
+                        Left . ErrOverride $
+                            "Type Conflict between: "
+                                ++ show term
+                                ++ ":"
+                                ++ show ty
+                                ++ " and "
+                                ++ show term'
+                                ++ ":"
+                                ++ show ty'
+
+
+
+flat :: Either a (Either a b) -> Either a b
+flat = either Left id
+
+
+-- | Pre parses the Term for primitives and adds their type to the context.
+buildContext :: Context -> Term -> Either TError Context
+buildContext eCtx =
+    let i = TCon "Int"
+        b = TCon "Bool"
+
+        to = (mempty :=>)
+
+        opType :: Operations -> T
+        opType = \case
+            Add -> TVec [i, i] :=> i
+            Subtract -> TVec [i, i] :=> i
+            If -> TVec[ b
+                      , TLoc (Lo "if") $ TVar "ifVar1"
+                      , TLoc (Lo "if") $ TVar "ifVar1"
+                      ] :=>
+                  TVec [ TLoc La $ TVar "ifVar1"]
+     in \case
+            V x St -> do
+                let rInt = (readMaybe x) :: Maybe Int
+                let rBool = (readMaybe x) :: Maybe Bool
+                let rOp = (readMaybe x) :: Maybe Operations
+                let nCtx = maybe [] (const [(x, to i)]) rInt
+                let nCtx' = maybe [] (const [(x, to b)]) rBool
+                let nCtx'' = maybe [] ((: []) . ((,) x) . opType) rOp
+                foldr (\m p -> flat $ mergeCtx <$> pure m <*> p) (pure []) $
+                    eCtx : nCtx : nCtx' : nCtx'' : []
+            V x t' -> do
+                let lCtx = buildContext eCtx (V x St)
+                let rCtx = buildContext eCtx t'
+                flat $ mergeCtx <$> lCtx <*> rCtx
+            P t _ t' -> do
+                let lCtx = buildContext eCtx t
+                let rCtx = buildContext eCtx t'
+                flat $ mergeCtx <$> lCtx <*> rCtx
+            B _ _ _ t -> buildContext eCtx t
+            St -> pure eCtx
+
+
+splitStream :: [a] -> ([a], [a])
+splitStream x = (,) l r
+  where
+    l = snd <$> (filter (odd . fst) $ zip ([1 ..] :: [Integer]) x)
+    r = snd <$> (filter (not . odd . fst) $ zip ([1 ..] :: [Integer]) x)
+
+
+freshTypeVar :: [T]
+freshTypeVar =
+    TVar
+        <$> [ mconcat $ [[x], show y]
+            | y <- [1 ..] :: [Integer]
+            , x <- ['a' .. 'z']
+            ]
+
+freshVarTypes :: [T]
+freshVarTypes = zipWith (:=>) ls rs
+  where
+    (ls,rs) = splitStream freshTypeVar
+
+
+-- | Normalise gets rid of empty Types at locations.
+normaliseT :: T -> T
+normaliseT t
+    | t == normalisedT = normalisedT
+    | otherwise = normaliseT normalisedT
+  where
+    normalisedT = normaliseT' t
+    normaliseT' = \case
+        TEmp -> mempty
+        TVec [] -> mempty
+        TLoc _ (TVec []) -> mempty
+        TLoc _ (TEmp) -> mempty
+        TLoc _ (TCon "") -> mempty
+        TLoc l (TVec (x : xs)) -> TLoc l x <> (TLoc l $ TVec xs)
+        TVec ([x]) -> normaliseT x
+        t1 :=> t2 -> normaliseT t1 :=> normaliseT t2
+        TVec (x : xs) -> normaliseT x <> (normaliseT $ TVec xs)
+        x -> x -- Just to be sure it gets through.
diff --git a/src/FMCt/Pretty.hs b/src/FMCt/Pretty.hs
index 5f0806e..dff90f2 100644
--- a/src/FMCt/Pretty.hs
+++ b/src/FMCt/Pretty.hs
@@ -1,11 +1,16 @@
 module FMCt.Pretty (
     printStack,
     printOutput,
+    printBindings2,
+    printBindingsA,
+    printSubs,
 ) where
 
 import Data.Map as M
 import FMCt.Evaluator
 import FMCt.Syntax
+import qualified FMCt.TypeChecker2 as T2
+import qualified FMCt.TypeCheckerAlt as TA
 
 printStack :: State -> String
 printStack (m, b) = "Memory: \n" ++ printer mem ++ "Bindings: \n" ++ printer bin
@@ -22,3 +27,19 @@ printOutput (m, _) = "Output: \n" ++ printer out
     printer = \case
         [] -> ""
         (x : xs) -> show x ++ "\n" ++ printer xs
+
+-- | Pretty Prints all the bindings in a context for derivation from TypeChecker 2.
+printBindings2 :: T2.Derivation -> String
+printBindings2 = auxCtxPP . T2.getContext
+
+-- | Pretty Prints all the bindings in a context for derivation from TypeChecker Alt.
+printBindingsA :: TA.Derivation -> String 
+printBindingsA = auxCtxPP . TA.getContext
+
+-- | Shared Pretty Printer.
+auxCtxPP :: [(String, T)] -> [Char]
+auxCtxPP = mconcat . fmap (\(b,t) -> mconcat [ " ", b, " : ", pShow t, "\n"])
+
+-- | Pretty Prints substitutions
+printSubs :: [T2.TSubs] -> String
+printSubs = mconcat . fmap (\(x,y) -> mconcat [" ", pShow x, " ~> ", pShow y, "\n"])
diff --git a/src/FMCt/TypeChecker.hs b/src/FMCt/TypeChecker.hs
index 6a92bad..598c150 100644
--- a/src/FMCt/TypeChecker.hs
+++ b/src/FMCt/TypeChecker.hs
@@ -20,7 +20,9 @@ module FMCt.TypeChecker (
     (<.>),
     getTermType,
     splitStream,
-    buildContext,    
+    buildContext,
+    pShow,
+    pShow',
 ) where
 
 --import Data.Set
@@ -565,3 +567,80 @@ instance Pretty Derivation where
                 (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ "  " ++ y | (x, y) <- zip d1 (extend (l2 + m2 + r2) d2)])
             | otherwise =
                 (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ " " ++ y | (x, y) <- zip (extend (l1 + m1 + r1) d1) d2])
+    pShow d = unlines (reverse strs)
+      where
+        (_, _, _, strs) = showD d
+        showT :: T -> String
+        showT = pShow
+        showC :: Context -> String
+        showC =
+            let sCtx (x, t) = show x ++ ":" ++ showT t ++ ", "
+             in \case
+                    [] -> []
+                    c -> (flip (++) " ") . mconcat $ sCtx <$> c
+        showJ :: Judgement -> String
+        showJ (cx, n, t) = mconcat $ showC cx{-"Γ "-} : "|- " : show n : " : " : showT t : []
+        showL :: Int -> Int -> Int -> String
+        showL l m r = mconcat $ replicate l ' ' : replicate m '-' : replicate r ' ' : []
+        showD :: Derivation -> (Int, Int, Int, [String])
+        showD (Star j) = (0, k, 0, [s, showL 0 k 0]) where s = showJ j; k = length s
+        showD (Variable j) = (0, k, 0, [s, showL 0 k 0]) where s = showJ j; k = length s
+        showD (Abstraction j d') = addrule (showJ j) (showD d')
+        showD (Application j d') = addrule (showJ j) (showD d')
+        showD (Fusion j d' e) = addrule (showJ j) (sidebyside (showD d') (showD e))
+        addrule :: String -> (Int, Int, Int, [String]) -> (Int, Int, Int, [String])
+        addrule x (l, m, r, xs)
+            | k <= m =
+                (ll, k, rr, (replicate ll ' ' ++ x ++ replicate rr ' ') : showL l m r : xs)
+            | k <= l + m + r =
+                (ll, k, rr, (replicate ll ' ' ++ x ++ replicate rr ' ') : showL ll k rr : xs)
+            | otherwise =
+                (0, k, 0, x : replicate k '-' : [replicate (- ll) ' ' ++ y ++ replicate (- rr) ' ' | y <- xs])
+          where
+            k = length x; i = div (m - k) 2; ll = l + i; rr = r + m - k - i
+        extend :: Int -> [String] -> [String]
+        extend i strs' = strs' ++ repeat (replicate i ' ')
+        sidebyside :: (Int, Int, Int, [String]) -> (Int, Int, Int, [String]) -> (Int, Int, Int, [String])
+        sidebyside (l1, m1, r1, d1) (l2, m2, r2, d2)
+            | length d1 > length d2 =
+                (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ "  " ++ y | (x, y) <- zip d1 (extend (l2 + m2 + r2) d2)])
+            | otherwise =
+                (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ " " ++ y | (x, y) <- zip (extend (l1 + m1 + r1) d1) d2])
+
+-- | Pretty Show of derivation hiding the context.
+pShow' :: Derivation -> String
+pShow' d = unlines (reverse strs)
+  where
+    (_, _, _, strs) = showD d
+    showT :: T -> String
+    showT = pShow
+    showC :: Context -> String
+    showC = const "Γ "
+    showJ :: Judgement -> String
+    showJ (cx, n, t) = mconcat $ showC cx : "|- " : pShow n : " : " : showT t : []
+    showL :: Int -> Int -> Int -> String
+    showL l m r = mconcat $ replicate l ' ' : replicate m '-' : replicate r ' ' : []
+    showD :: Derivation -> (Int, Int, Int, [String])
+    showD (Star j) = (0, k, 0, [s, showL 0 k 0]) where s = showJ j; k = length s
+    showD (Variable j) = (0, k, 0, [s, showL 0 k 0]) where s = showJ j; k = length s
+    showD (Abstraction j d') = addrule (showJ j) (showD d')
+    showD (Application j d') = addrule (showJ j) (showD d')
+    showD (Fusion j d' e) = addrule (showJ j) (sidebyside (showD d') (showD e))
+    addrule :: String -> (Int, Int, Int, [String]) -> (Int, Int, Int, [String])
+    addrule x (l, m, r, xs)
+        | k <= m =
+            (ll, k, rr, (replicate ll ' ' ++ x ++ replicate rr ' ') : showL l m r : xs)
+        | k <= l + m + r =
+            (ll, k, rr, (replicate ll ' ' ++ x ++ replicate rr ' ') : showL ll k rr : xs)
+        | otherwise =
+            (0, k, 0, x : replicate k '-' : [replicate (- ll) ' ' ++ y ++ replicate (- rr) ' ' | y <- xs])
+      where
+        k = length x; i = div (m - k) 2; ll = l + i; rr = r + m - k - i
+    extend :: Int -> [String] -> [String]
+    extend i strs' = strs' ++ repeat (replicate i ' ')
+    sidebyside :: (Int, Int, Int, [String]) -> (Int, Int, Int, [String]) -> (Int, Int, Int, [String])
+    sidebyside (l1, m1, r1, d1) (l2, m2, r2, d2)
+        | length d1 > length d2 =
+            (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ "  " ++ y | (x, y) <- zip d1 (extend (l2 + m2 + r2) d2)])
+        | otherwise =
+            (l1, m1 + r1 + 2 + l2 + m2, r2, [x ++ " " ++ y | (x, y) <- zip (extend (l1 + m1 + r1) d1) d2])
diff --git a/src/FMCt/TypeChecker2.hs b/src/FMCt/TypeChecker2.hs
index 174bed9..1be40a9 100644
--- a/src/FMCt/TypeChecker2.hs
+++ b/src/FMCt/TypeChecker2.hs
@@ -8,14 +8,18 @@ module FMCt.TypeChecker2
     Derivation(..),
     Judgement,
     Context,
+    TSubs,
     derive0,
     derive1,
     testD0,    
     testD1,
     testD2,
     derive2,
+    derive2Subs,
     getTermType,
     pShow',
+    normalForm,
+    getContext,
   ) where
 import FMCt.Syntax
 import FMCt.Parsing
@@ -38,9 +42,11 @@ type Context = [(Vv, T)]
 type Judgement = (Context, Term, T)
 
 type Term = Tm
-           
+
+-- | A type substitution is a pair of types             
 type TSubs = (T,T)
 
+-- | Standard Derivation type. Based on the FMC's BNF.
 data Derivation
     = Star        !Judgement
     | Variable    !Judgement !Derivation
@@ -48,9 +54,13 @@ data Derivation
     | Application !Judgement !Derivation !Derivation
     deriving (Show, Eq)
 
+-- | Default Empty Context
 emptyCx :: Context
 emptyCx = [("*",mempty :=> mempty)]
 
+-- | Converts a term into its normal form.
+-- Example:
+-- > a,l(al(b),a),c ~> a,c,l(a,al(b))
 normalForm :: T -> T
 normalForm = \x -> case x of 
   TEmp -> TEmp
@@ -67,7 +77,8 @@ normalForm = \x -> case x of
   TLoc l t -> TLoc l (normalForm t)
   m :=> n -> normalForm m :=> normalForm n
 
- 
+-- | Derive0 provides the structure of the derivation, without unifing the
+-- types. Useful for testing the AST of a type derivation.
 derive0 :: Term -> Derivation
 derive0 term = derive0' freshVarTypes term
   where
@@ -192,13 +203,21 @@ type Result a = Either TError a
 
 -- | Same as "derive1" but safe, and applies all substitutions at the end.
 derive2 :: Term -> Result Derivation
-derive2 term = do
+derive2 = (fmap snd) . derive2Aux
+
+-- | Get the substitutions that were needed for the unification.
+derive2Subs :: Term -> Result [TSubs]
+derive2Subs = (fmap fst) . derive2Aux
+
+-- | Same as "derive1" but safe, and applies all substitutions at the end.
+derive2Aux :: Term -> Result ([TSubs],Derivation)
+derive2Aux term = do
   let (ppTerm,lTStream) = replaceInfer freshVarTypes term
   bCx           <- pBCx ppTerm                             -- pre build context
   result        <- derive2' lTStream bCx emptySb ppTerm    -- derive
   let derivation = snd result                              -- take final derivation
   let casts      = fst result                              -- take the final casts 
-  return $ applyTSubsD casts derivation                    -- apply them to the derivation and return it 
+  return $ (casts,applyTSubsD casts derivation)            -- apply them to the derivation and return it 
   
   where
     emptySb = []
diff --git a/src/FMCt/TypeCheckerAlt.hs b/src/FMCt/TypeCheckerAlt.hs
new file mode 100644
index 0000000..ff4cecb
--- /dev/null
+++ b/src/FMCt/TypeCheckerAlt.hs
@@ -0,0 +1,382 @@
+{-# OPTIONS_GHC -Wno-unused-imports #-}
+{-# OPTIONS_GHC -Wno-unused-matches #-}
+{-# OPTIONS_GHC -Wno-unused-top-binds#-}
+
+-- |
+--Module      : Alternative Type Checker (Legacy}
+--
+--Description : Alternative Type Checker that uses a different set of derivation rules. 
+--
+--Alternative type-checker (legacy).
+
+module FMCt.TypeCheckerAlt ( derive1, testD1, getContext, Derivation(..), pShow')
+where 
+
+import FMCt.Syntax
+import FMCt.Parsing
+import FMCt.TypeChecker (
+  Derivation(..),
+  freshVarTypes,
+  splitStream,
+  TError(..),
+  normaliseT,
+  pShow',
+  buildContext,
+  Operations(..))
+import Control.Monad
+import FMCt.Aux.Pretty (pShow,Pretty)
+
+type Context = [(Vv, T)]
+
+type Term = Tm
+
+emptyCx :: Context
+emptyCx = [("*",mempty :=> mempty)]
+
+derive1 :: Term -> Either TError Derivation
+derive1 term = do
+  preBuildCtx <- buildContext emptyCx term
+  derive1' freshVarTypes preBuildCtx term
+  
+  where
+    
+    derive1' :: [T] -> Context -> Term -> Either TError Derivation
+    derive1' stream exCx = \case
+
+      St -> do 
+        ty <- getType St exCx
+        return $ Star (exCx, St, ty)
+      
+      xx@(V x St) -> do
+        ty <- getType xx exCx 
+        return $ Variable (exCx, xx, ty)        
+            
+      xx@(V bi tm) -> do
+        
+        let (lStr,rStr) = splitStream $ tail stream
+        derivL <- (derive1' lStr exCx (V bi St))
+        let lCx = getContext derivL
+        derivR <- (derive1' rStr lCx tm)          
+        let rCx = getContext derivR
+        let mCx = makeSet $ lCx ++ rCx          
+        let  tL = getDerivationT derivL
+        let  tR = getDerivationT derivR          
+        let (tCasts,ty) = fuse tL tR
+        return $ applyTSubsD tCasts $ Fusion (mCx, xx, ty) derivL derivR
+
+      xx@(B bi bTy lo St) -> do
+        let ty = TLoc lo bTy :=> mempty
+        let nCx = (bi,bTy) : exCx
+        deriv <- derive1' (tail stream) nCx (V bi St)
+        let aboveCx = getContext deriv
+        return $ Abstraction (aboveCx, xx, ty) deriv
+            
+      xx@(B bi bTy lo tm) -> do 
+        let (lStr,rStr) = splitStream $ tail stream
+        derivL <- (derive1' lStr exCx (B bi bTy lo St))
+        let lCx = getContext derivL
+        derivR <- derive1' rStr lCx tm
+        let rCx = getContext derivR
+        let mCx = makeSet $ lCx ++ rCx
+                    
+        let tL = getDerivationT derivL
+        let tR = getDerivationT derivR
+          
+        let (tCasts,ty) = fuse tL tR
+
+        return . applyTSubsD tCasts $ Fusion (mCx, xx, ty) derivL derivR
+
+      xx@(P ptm lo St) -> do
+        deriv <- derive1' (tail stream) exCx ptm
+        let abvT = getDerivationT  deriv
+        let ty = mempty :=> TLoc lo abvT
+        let aboveCx = getContext deriv
+        return $ Application (aboveCx, xx, ty) deriv 
+
+      xx@(P ptm lo tm) -> do 
+        let (lStr,rStr) = splitStream $ tail stream
+        derivL <- derive1' lStr exCx (P ptm lo St)
+        let lCx = getContext derivL
+        derivR <- derive1' rStr lCx tm
+        let rCx = getContext derivR
+        let mCx = makeSet $ lCx ++ rCx
+                    
+        let tL = getDerivationT derivL
+        let tR = getDerivationT derivR
+          
+        let (tCasts,ty) = fuse tL tR
+        return . applyTSubsD tCasts $ Fusion (mCx, xx, ty) derivL derivR
+
+testD1 :: String -> IO ()
+testD1 = either (putStrLn.show) putStrLn . fmap pShow . derive1 . parseFMC
+
+type TSubs = (T,T)
+
+consume :: [TSubs]       -- ^ Substitutions to be made in both types.
+        -> T             -- ^ The consuming Type.
+        -> T             -- ^ The consumed Type.
+        -> ([TSubs],T,T) -- ^ The new list of substitutions, remaining from the consuming, remaining from the consumed.
+consume exSubs x y =
+  let
+    x' = normaliseT $ applyTSub  exSubs x -- we use the already subtituted form when consuming
+    y' = normaliseT $ applyTSub  exSubs y -- for both terms
+  in
+    case x' of      
+      TEmp -> case y' of
+--        TVar _ -> ((y',x'):exSubs,mempty,mempty)
+        _ ->  (exSubs,mempty,y') -- mempty doesn't change anything else 
+      
+      TVec [] -> (exSubs,mempty,y') -- synonym for mempty
+      
+      TCon _ -> case y' of         
+        TEmp -> (exSubs,x',mempty)
+        TVec [] -> (exSubs,x',mempty)
+        TCon _ -> if x' == y'
+                  then (exSubs, mempty, mempty)
+                  else error $ "cannot consume! - type " ++ show y' ++ " should be " ++ show x'
+        TVec (yy': yys') -> 
+          let
+            (interSubs,interX,remainY) = consume exSubs x' yy'
+            (finalSubs,finalX,finalY) = consume interSubs interX (TVec yys')
+          in
+            (finalSubs,finalX,remainY <> finalY)
+        t1 :=> t2 ->  error $ show x' ++ " cannot consume higher type " ++ show y'
+        -- if a constant tries to consume a variable, it creates a substitution and gets fully consumed
+        TVar _ -> ((y',x') : exSubs, mempty, mempty) 
+        TLoc _ _ -> (exSubs,x',y')
+
+      TVar _ -> case y' of
+        TEmp -> ((x',y'):exSubs,mempty,mempty)
+        TVec [] -> (exSubs,x',mempty)
+        -- if consumed by anything, the Variable gets cast and changes all the
+        -- other appearances of itself.
+        _ -> (((x',y'):exSubs),mempty,mempty)
+
+      TLoc xl' xt' -> case y' of
+        TEmp -> (exSubs,x',mempty)
+        TVec [] -> (exSubs,x',mempty)
+        TCon _ -> (exSubs,x',y) -- home row and locations don't interact
+        TVar _ -> (exSubs,x',y) -- home row variable and locations don't interact
+        TVec (yy': yys') -> 
+          let
+            (interSubs,interX,remainY) = consume exSubs x' yy'
+            (finalSubs,finalX,finalY) = consume interSubs interX (TVec yys')
+          in
+            (finalSubs,finalX,remainY <> finalY)
+        TLoc yl' yt' -> if yl' == xl'
+                        then
+                          let
+                            (finalSubs, finalX', finalY') = consume exSubs xt' yt'
+                          in
+                            (finalSubs, TLoc xl' finalX', TLoc yl' finalY')
+                        else
+                          (exSubs,x',y)
+        _ :=> _ -> (exSubs,x',y)
+        
+      ix' :=> ox' -> case y' of
+        TEmp -> (exSubs,x',mempty)
+        TVec [] -> (exSubs,x',mempty)
+        TCon _ -> error $ "cannot fuse higer type " ++ show x' ++ " with " ++ show y'
+        TVar _ -> (((y',x'):exSubs),mempty,mempty)
+        TLoc _ _ -> (exSubs,x',y')
+        TVec (yy' : yys') ->
+          let
+            (interSubs, interX', interYY') = consume exSubs x' yy'
+            (finalSubs, finalX', finalYY') = consume interSubs interX' (TVec yys')
+          in
+            (finalSubs, finalX', interYY' <> finalYY')
+        iy' :=> oy' ->
+          if normaliseT x' == normaliseT y'
+             then (exSubs, mempty, mempty)
+             else let
+               (intSubs, leftIX', leftIY') =  consume exSubs ix' iy'
+               (finalSubs, rightIX', rightIY') =  consume intSubs ox' oy'
+               (finalL,finalR) = (normaliseT $ leftIX' <> leftIY', normaliseT $ rightIX' <> rightIY')
+               res = (finalSubs, finalL, finalR)
+--               res = (finalSubs,mempty,mempty)
+               in case res of
+                    (_,TEmp,TEmp) -> res
+                    
+                    _ -> error $ show x' ++ " cannot consume " ++ show y' ++ " fusion result: " ++ show res
+        
+      TVec (xx':xxs') -> case y' of
+        TEmp -> (exSubs,x',mempty)
+        TVec [] -> (exSubs,x',mempty)
+        TVec (_:_) ->
+          let
+            (interSubs, interXX', interY') = consume exSubs xx' y'
+            (finalSubs, finalXXs', finalY') = consume interSubs (TVec xxs') interY'
+          in
+            (finalSubs, interXX' <> finalXXs', finalY')
+            
+        -- The same way for all the other types. We recursively try the first of
+        -- the first vector with all of the second. 
+        _ -> 
+          let
+            (interSubs, interXX', interY') = consume exSubs xx' y'
+            (finalSubs, finalXXs', finalY') = consume interSubs (TVec xxs') interY'
+          in
+            (finalSubs, interXX' <> finalXXs', finalY')
+
+diffLoc :: T -> T -> Bool
+diffLoc = \case
+  x@(TCon _) -> \case
+    TCon _ -> False
+    TVar _ -> False -- Unsure about this
+    TEmp -> True
+    TVec [] -> True
+    TVec y -> diffLoc x `all` y
+    TLoc _ _ -> True
+    _ -> False 
+  x@(TVar _) -> \case
+    TLoc _ _ -> True
+    TEmp -> True
+    TVec [] -> True
+    TVec y -> diffLoc x `all` y
+    _ -> False
+  TVec [] -> const True
+  TEmp -> const True
+  xx@(TVec (x:xs)) -> \case
+    y@(TVec yy) -> diffLoc x `all` yy && (diffLoc (TVec xs) y)
+    y -> diffLoc y xx -- flip it
+  TLoc l _ -> \case
+    TLoc k _ -> if l == k then False else True
+    _ -> True
+  x@(_ :=> _) -> \y -> diffLoc y x
+    
+fuse :: T -> T -> ([TSubs],T)
+fuse = \case
+  x@(xi :=> xo) -> \case
+    y@(yi :=> yo) ->
+      let
+        (subs, remainY, remainX) = consume [] yi xo
+        res = (subs, normaliseT remainX, normaliseT remainY)
+      in
+        case res of
+--          _ -> error $ show res 
+          (_,TEmp,_) -> (,) subs ((xi <> remainY) :=> yo)
+          (_,_,TEmp) -> (,) subs (xi :=> (yo <> remainX))
+          _ -> if snd $ aux diffLoc [remainX, remainY, xi, yi]
+               then (,) subs ((xi <> remainY) :=> (yo <> remainX))
+               else error $ "cannot fuse " ++ show x ++ " "  ++ show y ++ " result: " ++ show res
+            where
+              aux :: Monoid a => (a -> a -> Bool) -> [a] -> (a,Bool)
+              aux f []  = (mempty,True)
+              aux f (z:zs)  = (z, (f z (fst $ aux f zs)) && (snd $ aux f zs))
+    y@(TVar _) ->
+      ([(y,x)],mempty)
+    y -> error $ "cannot fuse " ++ show x ++ " and " ++ show y ++ ". Wrong type Types - Use Function Types"
+  x -> \y -> error $ "cannot fuse " ++ show x ++ " and " ++ show y
+      
+applyTSub :: [TSubs] -> T -> T
+applyTSub = \case
+  [] -> id
+  xx@((xi,xo):xs) -> \case
+     TEmp -> TEmp
+     y@(TCon _ ) -> y
+     TLoc l t -> TLoc l (applyTSub xx t)
+     TVec y -> TVec $ applyTSub xx <$> y
+     yi :=> yo -> applyTSub xx yi :=> applyTSub xx yo
+     y@(TVar _) -> if y == xi then xo else applyTSub xs y
+
+{-
+The first derivation always can find a way to derive the term. Now we need a way
+ to specialise it. Given that we are not allowing for types to be re-cast we can
+ merge the context by creating our first round of substitutions.
+-}
+  
+       
+type Subs = [(T,T)]
+
+getType :: Term -> Context -> Either TError T
+getType = \case
+    t@(V b St) -> \case
+        [] ->
+            Left $
+                ErrUndefT $
+                    mconcat
+                        [ "Cannot Find type for binder: "
+                        , show b
+                        , " in context. Have you defined it prior to calling it ?"
+                        ]
+        ((b', ty) : xs) -> if b == b' then pure ty else getType t xs
+    St -> \_ -> pure $ mempty :=> mempty
+    t -> \_ ->
+        Left . ErrNotBinder $
+            mconcat ["Attempting to get type of:", show t]
+
+getContext :: Derivation -> Context
+getContext = \case
+  Star (c,_,_) -> c
+  Variable (c,_,_) -> c
+  Abstraction (c,_,_) _ -> c
+  Fusion (c,_,_) _ _ -> c
+  Application (c,_,_) _ -> c
+
+
+applySubsT :: Subs -> T -> T
+applySubsT [] x = x
+applySubsT ((ti,to):xs) x = if ti == x then applySubsT xs to else applySubsT xs x 
+
+applySubsCx :: Subs -> Context -> Context
+applySubsCx x y = applySubsVvT x <$> y
+
+applySubsVvT :: Subs -> (Vv,T) -> (Vv,T)
+applySubsVvT [] y = y
+applySubsVvT ((ti,to):xs) y@(yv,yt)
+  | yt == ti  = applySubsVvT xs (yv,to)
+  | otherwise = applySubsVvT xs y
+  
+applySubsD :: Subs -> Derivation -> Derivation
+applySubsD subs = \case
+  Star (cx,tm,ty) -> Star (applySubsCx subs cx, tm ,applySubsT subs ty)
+  Variable (cx,tm,ty) -> Variable (applySubsCx subs cx, tm ,applySubsT subs ty)
+  Abstraction (cx,tm,ty) de ->
+    Abstraction
+      (makeSet $ applySubsCx subs cx, tm ,applySubsT subs ty)
+        (applySubsD subs de)
+  Application (cx,tm,ty) de ->
+    Application
+      (makeSet $ applySubsCx subs cx, tm ,applySubsT subs ty)
+        (applySubsD subs de)
+  Fusion (cx,tm,ty) dL dR ->
+    Fusion
+      (makeSet $ applySubsCx subs cx, tm ,applySubsT subs ty)
+        (applySubsD subs dL)
+          (applySubsD subs dR)
+
+applyTSubsD :: [TSubs] -> Derivation -> Derivation
+applyTSubsD subs = \case 
+  Fusion (cx,tm,ty) dL dR -> Fusion ( (\(x,y)-> (x,applyTSub subs y)) <$> cx, nTm , applyTSub subs ty) dL dR
+    where
+      nTm = case tm of
+        B v ty' l t' -> B v (applyTSub subs ty') l t'
+        x -> x
+          
+  _ -> error "You are not allowed to cast here! - this should never happen"
+  
+allCtx :: Derivation -> Context
+allCtx = \case
+  x@(Star _) -> getContext x
+  x@(Variable _) -> getContext x
+  x@(Application _ d) -> getContext x ++ allCtx d
+  x@(Abstraction _ d) -> getContext x ++ allCtx d
+  x@(Fusion _ dL dR) -> getContext x ++ allCtx dR ++ allCtx dL
+
+makeSet :: Eq a => [a] -> [a]
+makeSet []     = [] 
+makeSet (x:xs) = if elem x xs then makeSet xs else x : makeSet xs
+
+getDerivationT :: Derivation -> T
+getDerivationT = \case 
+  Star (_,_,t) -> t
+  Variable (_,_,t) -> t
+  Application (_,_,t) _ -> t
+  Abstraction (_,_,t) _ -> t
+  Fusion (_,_,t) _ _ -> t
+
+getLocation :: Term -> Lo
+getLocation = \case
+  P _ l _ -> l
+  B _ _ l _ -> l
+  x -> error $ "should't be reaching for location in term: " ++ show x
diff --git a/src/FMCt/Web/Components/MainPage.hs b/src/FMCt/Web/Components/MainPage.hs
index 03c74d3..e653465 100644
--- a/src/FMCt/Web/Components/MainPage.hs
+++ b/src/FMCt/Web/Components/MainPage.hs
@@ -18,7 +18,7 @@ mainPage = LU.renderText sMainPage
         LB.container_ $ do
             LB.row_ $ do
                 LB.span2_ $ LU.div_ [LU.name_ "Title"] $ LU.h1_ "FMCt-Web"
-                LB.span2_ $ LU.div_ [LU.name_ "SubTitle"] $ LU.h2_ "V.0.4.1.beta"
+                LB.span2_ $ LU.div_ [LU.name_ "SubTitle"] $ LU.h2_ "V.2.0.2.beta"
                 LU.hr_ []
                 LB.span2_ $ LU.h3_ "Welcome to the FMCt Web Interpreter."
 
@@ -27,5 +27,5 @@ mainPage = LU.renderText sMainPage
                 LB.span2_ $
                     LU.div_ [LU.name_ "Links"] $ do
                         LU.h3_ "Links"
-                        LU.ul_ $ LU.a_ [LU.href_ "parse?term=*"] "Parser"
+--                        LU.ul_ $ LU.a_ [LU.href_ "parse?term=*"] "Parser" -- Broken this is 
                         LU.ul_ $ LU.a_ [LU.href_ "derive?term=*"] "Derivation Tester"
diff --git a/src/FMCt/Web/MainWebsite.hs b/src/FMCt/Web/MainWebsite.hs
index d771a0c..a9f8fea 100644
--- a/src/FMCt/Web/MainWebsite.hs
+++ b/src/FMCt/Web/MainWebsite.hs
@@ -4,6 +4,7 @@ module FMCt.Web.MainWebsite (mainWebsite, mainWebsitePort) where
 
 import FMCt.Web.Helpers.Heroku (herokuGetPort)
 import FMCt.Web.Pages.Derive (pDerive)
+import qualified FMCt.Web.Pages.DeriveAlt as Da (pDerive)
 import FMCt.Web.Pages.Evaluator (pEvaluator)
 import FMCt.Web.Pages.Root (pRoot)
 import FMCt.Web.Style.MainStyle (mainStylePage)
@@ -25,6 +26,11 @@ mainWebsitePort port = do
             term' <- param "term"
             (html . LU.renderText . pDerive) term'
 
+    -- Alt Derivation Page.
+    let rDerivationPageAlt = get "/deriveAlt" $ do
+            term' <- param "term"
+            (html . LU.renderText . Da.pDerive) term'
+
     -- Styling.
     let css = S.get "/style.css" $ html mainStylePage    
 
@@ -34,6 +40,7 @@ mainWebsitePort port = do
         rParse
         css
         rDerivationPage
+        rDerivationPageAlt
 
 
 -- | Start serving the website.
diff --git a/src/FMCt/Web/Pages/Derive.hs b/src/FMCt/Web/Pages/Derive.hs
index 574937d..1207547 100644
--- a/src/FMCt/Web/Pages/Derive.hs
+++ b/src/FMCt/Web/Pages/Derive.hs
@@ -3,7 +3,9 @@ module FMCt.Web.Pages.Derive (pDerive) where
 import Data.List (unfoldr)
 import qualified Data.Text.Lazy as LA
 import FMCt (derive2, pShow, getTermType, pShow')
+import FMCt.TypeChecker2 (derive2Subs)
 import FMCt.Parsing (parseFMC')
+import FMCt.Pretty (printBindings2, printSubs)
 import FMCt.Web.Components.Brick (brick)
 import FMCt.Web.Components.RegularPage (regularPage)
 import qualified Lucid as LU
@@ -23,6 +25,8 @@ pDerive term = sDerivePage
             parsedBox
             termTypeBox
             derivationBox
+            bindgingTypeBox
+            subsTypeBox
 
     termForm :: LU.Html ()
     termForm = do
@@ -52,8 +56,35 @@ pDerive term = sDerivePage
                 deriv = case getTermType pTerm of
                   Left e -> show e 
                   Right ty -> pShow pTerm ++ " : "++ pShow ty                                  
-                
 
+    bindgingTypeBox :: LU.Html ()
+    bindgingTypeBox =
+        case (parseFMC' . LA.unpack) term of
+            Left _ -> pure ()
+            Right pTerm ->
+              brick
+                ("types-div" :: String)
+                ("Variables & Types" :: LA.Text)
+                ("Each variable has the following (inferred) type in the context" :: LA.Text)
+                types
+              where
+                types = either mempty (rBr . printBindings2) $ derive2 pTerm
+
+    subsTypeBox :: LU.Html ()
+    subsTypeBox =
+        case (parseFMC' . LA.unpack) term of
+            Left _ -> pure ()
+            Right pTerm ->
+              brick
+                ("subs-div" :: String)
+                ("Substitutions" :: LA.Text)
+                ("Substitutions needed to derive the term:" :: LA.Text)
+                subs
+              where
+                subs = either mempty (rBr . printSubs) $ derive2Subs pTerm
+                
+    -- | Utility function that re-writes whitespaces and newlines so that they
+    -- display correctly in HTML.
     rBr :: String -> LU.Html ()
     rBr str = aux spStr
       where
diff --git a/src/FMCt/Web/Pages/DeriveAlt.hs b/src/FMCt/Web/Pages/DeriveAlt.hs
new file mode 100644
index 0000000..f06b9ef
--- /dev/null
+++ b/src/FMCt/Web/Pages/DeriveAlt.hs
@@ -0,0 +1,92 @@
+module FMCt.Web.Pages.DeriveAlt (pDerive) where
+
+import Data.List (unfoldr)
+import qualified Data.Text.Lazy as LA
+import FMCt (pShow, getTermType)
+import FMCt.TypeCheckerAlt (pShow', derive1)
+import FMCt.Parsing (parseFMC')
+import FMCt.Pretty  (printBindingsA, printSubs)
+import FMCt.Web.Components.Brick (brick)
+import FMCt.Web.Components.RegularPage (regularPage)
+import qualified Lucid as LU
+import qualified Lucid.Bootstrap as LB
+
+pDerive :: LA.Text -> LU.Html ()
+pDerive term = sDerivePage
+  where
+    sDerivePage :: LU.Html ()
+    sDerivePage = do
+        regularPage ("Derivator (Legacy)" :: LA.Text) $ LB.span1_ page
+
+    page :: LU.Html ()
+    page = do
+        LU.body_ $ do
+            termForm
+            parsedBox
+            termTypeBox
+            derivationBox
+            bindgingTypeBox
+
+    termForm :: LU.Html ()
+    termForm = do
+        LU.hr_ []
+        LU.div_ [LU.name_ "term-div"] $ LU.form_ [LU.action_ "deriveAlt"] $ LU.input_ [LU.type_ "text", LU.name_ "term"]
+
+    parsedBox :: LU.Html ()
+    parsedBox =
+        brick ("parsed-div" :: LA.Text) ("Parsed Term" :: LA.Text) ("" :: LA.Text) pTerm
+      where
+        pTerm = either (LU.toHtml . show) (LU.toHtml . pShow) $ (parseFMC' . LA.unpack) term
+
+    derivationBox :: LU.Html ()
+    derivationBox =
+        case (parseFMC' . LA.unpack) term of
+            Left e -> LU.toHtml . show $ e
+            Right pTerm -> brick ("parsed-div" :: String) ("Term Derivation (Legacy)" :: LA.Text) ("" :: LA.Text) deriv
+              where
+                deriv = either (rBr . show) (rBr . pShow') $ derive1 pTerm
+
+    termTypeBox :: LU.Html ()
+    termTypeBox =
+        case (parseFMC' . LA.unpack) term of
+            Left e -> LU.toHtml . show $ e
+            Right pTerm -> brick ("parsed-div" :: String) ("Term-Type (Legacy)" :: LA.Text) ("" :: LA.Text) deriv
+              where
+                deriv = case getTermType pTerm of
+                  Left e -> show e 
+                  Right ty -> pShow pTerm ++ " : "++ pShow ty                                  
+
+    bindgingTypeBox :: LU.Html ()
+    bindgingTypeBox =
+        case (parseFMC' . LA.unpack) term of
+            Left _ -> pure ()
+            Right pTerm ->
+              brick
+                ("types-div" :: String)
+                ("Variables & Types (Legacy)" :: LA.Text)
+                ("Each variable has the following (inferred) type in the context" :: LA.Text)
+                types
+              where
+                types = either mempty (rBr . printBindingsA) $ derive1 pTerm
+                
+    -- | Utility function that re-writes whitespaces and newlines so that they
+    -- display correctly in HTML.
+    rBr :: String -> LU.Html ()
+    rBr str = aux spStr
+      where
+        aux = \case
+            [] -> LU.hr_ []
+            (x : xs) -> LU.p_ [] (LU.toHtml x) >> aux xs
+
+        separateBy :: Eq a => a -> [a] -> [[a]]
+        separateBy chr = unfoldr sep
+          where
+            sep [] = Nothing
+            sep l = Just . fmap (drop 1) . break (== chr) $ l
+
+        spStr = separateBy '\n' $ replaceSp str
+
+        replaceSp [] = []
+        replaceSp (' ' : xs) = ' ' : replaceSp xs
+        -- space taken from https://qwerty.dev/whitespace/
+        replaceSp (x : xs) = x : replaceSp xs
diff --git a/src/FMCt/Web/Pages/Root.hs b/src/FMCt/Web/Pages/Root.hs
index 37c308a..18b6803 100644
--- a/src/FMCt/Web/Pages/Root.hs
+++ b/src/FMCt/Web/Pages/Root.hs
@@ -12,12 +12,13 @@ pRoot = sMainPage
   where
     sMainPage :: LU.Html ()
     sMainPage = do
-        regularPage "FMCt Homepage" $ do
-            brick "version" "V.0.0.1" "" "Welcome to the FMCt Web Interpreter."
-            brick "version" "V.0.0.1" "" "Links"
+        regularPage ("FMCt Homepage"::String) $ do
+            brick ("version"::String) ("V.2.0.1"::String) (""::String) ("Welcome to the FMCt Web Interpreter." :: String)
             LB.row_ $ do
                 LB.span2_ $
                     LU.div_ [LU.name_ "Links"] $ do
                         LU.h3_ "Links"
-                        LU.ul_ $ LU.a_ [LU.href_ "parse?term=*"] "Parser"
+--                        LU.ul_ $ LU.a_ [LU.href_ "parse?term=*"] "Parser" 
+--                        Evaluator has fallen a bit behind. TODO fix
                         LU.ul_ $ LU.a_ [LU.href_ "derive?term=*"] "Derivation Tester"
+                        LU.ul_ $ LU.a_ [LU.href_ "deriveAlt?term=*"] "Derivation Tester (Legacy)"