diff --git a/Choice.hs b/Choice.hs
--- a/Choice.hs
+++ b/Choice.hs
@@ -30,13 +30,16 @@
   pure = Success
   mf <*> ma = mf >>= (<$> ma)
 
+--determine a b = appendErr "" $ (:<|>:) (appendErr "" a) (appendErr "" b)
+determine = (:<|>:)
+
 instance Alternative Choice where
   empty = Fail ""
-  (<|>) = (:<|>:)
+  (<|>) = determine
 
 instance MonadPlus Choice where
   mzero = Fail ""
-  mplus = (:<|>:)
+  mplus = determine
 
 class RunChoice m where
   runError :: m a -> Either String a
diff --git a/Context.hs b/Context.hs
--- a/Context.hs
+++ b/Context.hs
@@ -62,16 +62,16 @@
 addToContext s c (Binding _ _ _ Nothing Nothing) = error $ "context not empty so can't add to tail: "++show c
 addToContext s c@(Context h ctxt t) elm@(Binding _ nm _ t'@(Just p) Nothing) | t' == t = checkContext (s++"\naddToCtxt J N: "++show elm ++ "\n\tOLD CONTEXT: "++show c) $ 
   Context h (M.insert p t'val $ M.insert nm elm $ ctxt) (Just nm)
-  where t'val = (lookupWith "looking up p ctxt" p ctxt) { elmNext = Just nm }
+  where t'val = (lookupWith (s++" looking up p ctxt") p ctxt) { elmNext = Just nm }
 addToContext s _ (Binding _ _ _ _ Nothing) = error "can't add this to tail"
 addToContext s (Context h ctxt t) elm@(Binding _ nm _ Nothing h'@(Just n)) | h' == h = checkContext (s++"\naddToCtxt N J: ") $ 
   Context (Just nm) (M.insert n h'val $ M.insert nm elm $ ctxt) t
-  where h'val = (lookupWith "looking up n ctxt" n ctxt) { elmPrev = Just nm }
+  where h'val = (lookupWith (s++" looking up n ctxt") n ctxt) { elmPrev = Just nm }
 addToContext s _ (Binding _ _ _ Nothing _) = error "can't add this to head"
 addToContext s ctxt@Context{ctxtMap = cmap} elm@(Binding _ nm _ (Just p) (Just n)) = checkContext (s++"\naddToCtxt J J: ") $ 
   ctxt { ctxtMap = M.insert n n'val $ M.insert p p'val $ M.insert nm elm $ cmap }
-  where n'val = (lookupWith "looking up n cmap" n cmap) { elmPrev = Just nm }
-        p'val = (lookupWith "looking up p cmap" p cmap) { elmNext = Just nm }
+  where n'val = (lookupWith (s++" looking up n cmap") n cmap) { elmPrev = Just nm }
+        p'val = (lookupWith (s++" looking up p cmap") p cmap) { elmNext = Just nm }
   
 removeFromContext :: Name -> Context -> Context
 removeFromContext nm ctxt@(Context h cmap t) = case M.lookup nm cmap of
@@ -90,15 +90,23 @@
           p' = M.insert cp $ (lookupWith "looking up a cmap for p'" cp cmap ) { elmNext = Just cn }
   where isSane bool a = if bool then a else error "This doesn't match intended binding"
 
+addAfter s t quant nm tp ctxt@Context{ctxtMap = cmap} = checkContext "addAfter" $ do
+  let top = lookupWith ("looking up "++t++"\n\t in context: "++show cmap++"\n\t"++s) t cmap
+  addToContext ("ADD_AFTER: "++s) ctxt $ Binding quant nm tp (Just $ elmName top) (elmNext top)
+
+addBefore s b quant nm tp ctxt@Context{ctxtMap = cmap} = checkContext "addBefore" $ do
+  let bot = lookupWith ("looking up "++b++"\n\t in context: "++show cmap++"\n\t"++s) b cmap
+  addToContext ("ADD_BEFORE: "++s) ctxt $ Binding quant nm tp (elmPrev bot) (Just $ elmName bot)
+
 addToHead s quant nm tp ctxt@Context{ctxtMap = cmap} = case M.lookup nm cmap of 
-  Nothing -> addToContext s ctxt $ Binding quant nm tp Nothing (ctxtHead ctxt)
+  Nothing -> addToContext ("ATH: "++s) ctxt $ Binding quant nm tp Nothing (ctxtHead ctxt)
   Just (Binding{ elmQuant = quant', elmType = tp'}) | quant' == quant && tp' == tp && quant == Forall -> 
-    addToContext s ctxt' $ Binding quant nm tp Nothing (ctxtHead ctxt')
+    addToContext ("ATH2: "++s) ctxt' $ Binding quant nm tp Nothing (ctxtHead ctxt')
     where ctxt' = removeFromContext nm ctxt
   _ -> error $ "Can't add to head, already in context: "++show nm++" : "++show tp++"\n@"++show ctxt
   
 addToTail s quant nm tp ctxt@Context{ctxtMap = cmap} = case M.lookup nm cmap of
-  Nothing -> addToContext s ctxt $ Binding quant nm tp (ctxtTail ctxt) Nothing
+  Nothing -> addToContext ("ATT: "++s) ctxt $ Binding quant nm tp (ctxtTail ctxt) Nothing
   Just (Binding{ elmQuant = quant', elmType = tp'}) | quant' == quant && tp' == tp && quant == Forall -> ctxt
   _ -> error $ "Can't add to tail, already in context: "++show nm++" : "++show tp++"\n@"++show ctxt
 
@@ -117,8 +125,8 @@
 getHead (Context Nothing _ _) = error "no head"
 
 -- gets the list of bindings after (below) a given binding
-getAfter s bind ctx = tail $ getAfter' s bind ctx            
-getAfter' s bind ctx@(Context{ ctxtMap = ctxt }) = gb bind
+getAfter s bind ctx = tail $ getAfterInclusive s bind ctx            
+getAfterInclusive s bind ctx@(Context{ ctxtMap = ctxt }) = gb bind
   where gb ~(Binding quant nm ty _ n) = (quant, (nm,ty)):case n of
           Nothing -> []
           Just n -> gb $ case M.lookup n ctxt of 
@@ -126,23 +134,23 @@
             Just c -> c
 
 -- gets the list of bindings before (above) a given binding
-getBefore s bind ctx = tail $ getBefore' s bind ctx            
-getBefore' s bind ctx@(Context{ ctxtMap = ctxt }) = gb bind
+getBefore s bind ctx = tail $ getBeforeInclusive s bind ctx            
+getBeforeInclusive s bind ctx@(Context{ ctxtMap = ctxt }) = gb bind
   where gb ~(Binding quant nm ty p _) = (quant, (nm,ty)):case p of
           Nothing -> []
           Just p -> gb $ case M.lookup p ctxt of 
             Nothing -> error $ "element "++show p++" not in map \n\twith ctxt: "++show ctx++" \n\t for bind: "++show bind++"\n\t"++s
             Just c -> c
 
---checkContext _ c = c
-
+checkContext _ c = c
+{-
 checkContext _ c@(Context Nothing _ Nothing) = c
 checkContext s ctx = foldr (\v c -> seq (checkEquals v) c) ctx $ zip st (reverse $ ta)
-  where st = getBefore' s (getTail ctx) ctx
-        ta = getAfter' s (getHead ctx) ctx
+  where st = getBeforeInclusive s (getTail ctx) ctx
+        ta = getAfterInclusive s (getHead ctx) ctx
         checkEquals (a,b) | (a == b) = ()
         checkEquals (a,b) = error $ s++" \n\tNOT THE SAME" ++show (a,b) ++ " \n\t IN "++show ctx
-
+-}
 
 -------------------------
 ---  Traversal Monad  ---
@@ -183,13 +191,32 @@
   case ty of
     Nothing -> Left <$> (\ctxt -> lookupWith ("looking up "++x++"\n\t in context: "++show ctxt++"\n\t"++s) x ctxt) <$> ctxtMap <$> stateCtxt <$> get
     Just a -> return $ Right a
+  
+getBindings :: Binding -> Env [(Name,Type)]
+getBindings bind = fmap snd <$> getQuantBindings bind
 
+getBindingsInclusive :: Binding -> Env [(Name,Type)]
+getBindingsInclusive bind = fmap snd <$> getQuantBindings bind
+
 -- | This gets all the bindings outside of a given bind and returns them in a list (not including that binding).
-getBindings :: Binding -> Env [(Name,Type)]
-getBindings bind = do
+getQuantBindings :: Binding -> Env [(Quant, (Name,Type))]
+getQuantBindings bind = do
   ctx <- stateCtxt <$> get
-  return $ snd <$> getBefore "IN: getBindings" bind ctx
+  return $ getBefore "IN: getQuantBindings" bind ctx
   
+getQuantBindingsInclusive :: Binding -> Env [(Quant, (Name,Type))]
+getQuantBindingsInclusive bind = do
+  ctx <- stateCtxt <$> get
+  return $ getBeforeInclusive "IN: getQuantBindingsInclusive" bind ctx  
+    
+  
+getBindingsBetween :: Binding -> Binding -> Env [(Name,Type)]
+getBindingsBetween top bottom = do
+  above <- getBindings top
+  target <- getBindings bottom
+  let aboveSet = S.insert (elmName top) $ S.fromList $ fst <$> above 
+  return $ filter (\n -> not $ S.member (fst n) aboveSet) target
+  
 getAnExist :: Env (Maybe (Name,Type))
 getAnExist = do
   ctx <- stateCtxt <$> get
@@ -197,19 +224,32 @@
       last = (elmQuant til, (elmName til, elmType til))
   return $ case ctx of
     Context _ _ Nothing -> Nothing
-    _ -> snd <$> find (\(q,_) -> q == Exists) (last:getBefore "IN: getBindings" til ctx)
+    _ -> snd <$> find (\(q,_) -> q == Exists) (last:getBefore "IN: getAnExist" til ctx)
 
+-- | `getAllBindings` gets all bindings, listed from tightest to loosest
+-- ie, ∀a:t∃b:t will return [(∃,(b,t)), (∀,(a,t))]
 getAllBindings = do
   ctx <- stateCtxt <$> get
   case ctx of
     Context _ _ Nothing -> return []
-    _ -> (getBindings $ getTail ctx)
+    _ -> getQuantBindingsInclusive $ getTail ctx
+
     
 getForalls :: Env ContextMap
 getForalls = do
   ctx <- ctxtMap <$> stateCtxt <$> get
   return $ anonymous <$> elmType <$> M.filter (\q -> elmQuant q == Forall) ctx
+
+getForallsAfter :: Binding -> Env (S.Set Name)
+getForallsAfter bind = do
+  ctx <- stateCtxt <$> get
+  return $ S.fromList $ map (fst . snd) $ filter ((== Forall) . fst) $ getAfter "IN: getForalls" bind ctx
   
+getExistsAfter :: Binding -> Env (S.Set Name)
+getExistsAfter bind = do
+  ctx <- stateCtxt <$> get
+  return $ S.fromList $ map (fst . snd) $ filter ((== Exists) . fst) $ getAfter "IN: getExistsAfter" bind ctx      
+
 getExists :: Env ContextMap
 getExists = do
   ctx <- ctxtMap <$> stateCtxt <$> get
diff --git a/HOU.hs b/HOU.hs
--- a/HOU.hs
+++ b/HOU.hs
@@ -88,14 +88,15 @@
                       let !sub'' = sub *** sub'
                       modifyCtxt $ subst sub'
                       uniWhile sub'' $! c'
-              
-              
-        vtrace 3 ("CONST: "++show c)
-          ( uniWith unifyOne 
+        
+        ctxt <- getAllBindings
+        
+        vtraceShow 2 3 "CONST" c 
+          $ vtraceShow 3 3 "CTXT" (reverse ctxt)
+          $ uniWith unifyOne 
           $ uniWith unifySearch
           $ uniWith unifySearchAtom
-          $ checkFinished c >> 
-          return (sub, c))
+          $ checkFinished c >> return (sub, c)
 
   sub <- fst <$> uniWhile mempty cons
   
@@ -165,28 +166,38 @@
     return $ Just (mempty, [s `apply` var nm :=: s'], False)
 
   (s , s') | s == s' -> vtrace 1 "-eq-" $ return $ Just (mempty, [], False)
-  (s@(Spine x yl), s') -> vtrace 4 "-ss-" $ do
+  (s@(Spine x yl), s') -> vtraceShow 4 5 "-ss-" cons $ do
     bind <- getElm ("all: "++show cons) x
     case bind of
-      Left bind@Binding{ elmQuant = Exists } -> vtrace 4 "-g?-" $ do
-        raiseToTop bind (Spine x yl) $ \(a@(Spine x yl),ty) sub ->
-          case subst sub s' of
-            b@(Spine x' y'l) -> vtrace 4 "-gs-" $ do
+      Left bind@Binding{ elmQuant = Exists, elmType = ty } -> vtraceShow 4 5 "-g?-" cons $ do
+        fors <- getForallsAfter bind
+        exis <- getExistsAfter bind
+        case s' of
+            b@(Spine x' y'l) -> vtraceShow 4 5 "-gs-" cons $ do
               bind' <- getElm ("gvar-blah: "++show cons) x' 
               case bind' of
                 Right ty' -> vtraceShow 1 2 "-gc-" cons $ -- gvar-const
---                  if allElementsAreVariables yl
---                  then gvar_const (Spine x yl, ty) (Spine x' y'l, ty')  
---                   else return Nothing
-                  gvar_const (Spine x yl, ty) (Spine x' y'l, ty') 
-                Left Binding{ elmQuant = Forall } | not $ S.member x' $ freeVariables yl -> 
-                  throwTrace 0 $ "CANT: gvar-uvar-depends: "++show (a :=: b)
+                  if allElementsAreVariablesNoPP fors yl
+                  then gvar_const (Spine x yl, ty) (Spine x' y'l, ty')  
+                  else return Nothing
+                Left Binding{ elmQuant = Forall } | (not $ elem (var x') yl) && S.member x' fors -> 
+                  if allElementsAreVariables fors yl 
+                  then throwTrace 0 $ "CANT: gvar-uvar-depends: "++show (a :=: b)
+                  else return Nothing
                 Left Binding{ elmQuant = Forall } | S.member x $ freeVariables y'l -> 
-                  throwTrace 0 $ "CANT: occurs check: "++show (a :=: b)
-                Left Binding{ elmQuant = Forall, elmType = ty' } -> vtrace 1 "-gui-" $  -- gvar-uvar-inside
-                  gvar_uvar_inside (Spine x yl, ty) (Spine x' y'l, ty')
-                Left bind@Binding{ elmQuant = Exists, elmType = ty' } -> 
-                  if not $ allElementsAreVariables yl && allElementsAreVariables y'l 
+                  if allElementsAreVariables fors yl 
+                  then throwTrace 0 $ "CANT: occurs check: "++show (a :=: b)
+                  else return Nothing
+                Left Binding{ elmQuant = Forall, elmType = ty' } | S.member x' fors -> vtraceShow 1 5 "-gui-" cons $  -- gvar-uvar-inside
+                  if allElementsAreVariables fors yl
+                  then gvar_uvar_inside (Spine x yl, ty) (Spine x' y'l, ty')
+                  else return Nothing
+                Left Binding{ elmQuant = Forall, elmType = ty' } -> vtraceShow 1 5 "-guo-" cons $ 
+                  if allElementsAreVariablesNoPP fors yl
+                  then gvar_uvar_outside (Spine x yl, ty) (Spine x' y'l, ty')
+                  else return Nothing
+                Left bind'@Binding{ elmQuant = Exists, elmType = ty'} -> vtraceShow 4 5 "-gg-" cons $
+                  if not $ allElementsAreVariables fors yl && allElementsAreVariables fors y'l && S.member x' exis
                   then return Nothing 
                   else if x == x' 
                        then vtraceShow 1 2 "-ggs-" cons $ -- gvar-gvar-same
@@ -194,8 +205,8 @@
                        else -- gvar-gvar-diff
                          if S.member x $ freeVariables y'l 
                          then throwTrace 0 $ "CANT: ggd-occurs check: "++show (a :=: b)
-                         else vtraceShow 1 2 "-ggd-" cons $ gvar_gvar_diff (Spine x yl, ty) (Spine x' y'l, ty') bind
-            _ -> vtrace 1 "-ggs-" $ return Nothing
+                         else vtraceShow 1 2 "-ggd-" cons $ gvar_gvar_diff bind (Spine x yl, ty) (Spine x' y'l, ty') bind'
+            _ -> vtraceShow 1 5 "-ggs-" cons $ return Nothing
       _ -> vtrace 4 "-u?-" $ case s' of 
         b@(Spine x' _) | x /= x' -> do
           bind' <- getElm ("const case: "++show cons) x'
@@ -212,16 +223,24 @@
               match al (Spine "#tycon#" [Spine _ [_]]:bl) = match al bl 
               match (a:al) (b:bl) = ((a :=: b) :) <$> match al bl 
               match [] [] = return []
-              match _ _ = throwTrace 0 $ "CANT: different numbers of arguments on constant: "++show cons
+              match _ _ = throwTrace 0 $ "CANT: different numbers of arguments: "++show cons
 
           cons <- match yl yl'
           return $ Just (mempty, cons, False)
         _ -> throwTrace 0 $ "CANT: uvar against a pi WITH CONS "++show cons
             
-allElementsAreVariables :: [Spine] -> Bool
-allElementsAreVariables = all $ \c -> case c of
-  Spine _ [] -> True
-  _ -> False
+allElementsAreVariables :: S.Set Name -> [Spine] -> Bool
+allElementsAreVariables fors = partialPerm mempty 
+  where partialPerm s [] = True
+        partialPerm s (Spine nm []:l) | S.member nm fors && not (S.member nm s) = 
+          partialPerm (S.insert nm s) l
+        partialPerm _ _ = False
+        
+allElementsAreVariablesNoPP fors = partial
+  where partial [] = True
+        partial (Spine nm []:l) | S.member nm fors = partial l
+        partial _ = False
+        
 
 typeToListOfTypes (Spine "#forall#" [_, Abs x ty l]) = (x,ty):typeToListOfTypes l
 typeToListOfTypes (Spine _ _) = []
@@ -230,9 +249,10 @@
 -- the problem WAS (hopefully) here that the binds were getting
 -- a different number of substitutions than the constraints were.
 -- make sure to check that this is right in the future.
-raiseToTop bind@Binding{ elmName = x, elmType = ty } sp m = do
-  
-  hl <- reverse <$> getBindings bind
+raiseToTop top@Binding{ elmNext = Just k}  bind@Binding{ elmName = x, elmType = ty } sp m | k == x = 
+  m (sp, ty) mempty
+raiseToTop top bind@Binding{ elmName = x, elmType = ty } sp m = do
+  hl <- reverse <$> getBindingsBetween top bind
   x' <- getNewWith "@newx"
   
   let newx_args = map (var . fst) hl
@@ -248,7 +268,7 @@
         modifyCtxt $ subst sub'
         return $ Just (sub'', cons,b)
         
-  modifyCtxt $ addToHead "-rtt-" Exists x' ty' . removeFromContext x
+  modifyCtxt $ addAfter "-rtt-" (elmName top) Exists x' ty' . removeFromContext x
   vtrace 3 ("RAISING: "++x' ++" +@+ "++ show newx_args ++ " ::: "++show ty'
          ++"\nFROM: "++x ++" ::: "++ show ty
           ) modifyCtxt $ subst sub
@@ -281,19 +301,21 @@
       
       sub = x |-> l
       
-  modifyCtxt $ addToHead "-ggs-" Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!
+  modifyCtxt $ addBefore "-ggs-" x Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!
+  modifyCtxt $ removeFromContext x
   
   return $ Just (sub, [], False) -- var xN :@: xNty])
   
 gvar_gvar_same _ _ = error "gvar-gvar-same is not made for this case"
 
-gvar_gvar_diff (a',aty') (sp, _) bind = raiseToTop bind sp $ \(b'@(Spine x' y'l), bty) subO -> do
+gvar_gvar_diff top (a',aty') (sp, _) bind = raiseToTop top bind sp $ \b subO -> do
+  let a = (subst subO a', subst subO aty')
+  gvar_gvar_diff' a b
   
-  let (Spine x yl, aty) = (subst subO a', subst subO aty')
-
+gvar_gvar_diff'  (Spine x yl, aty) ((Spine x' y'l), bty) = do
       -- now x' comes before x 
       -- but we no longer care since I tested it, and switching them twice reduces to original
-      n = length yl
+  let n = length yl
       m = length y'l
       
   aty <- regenAbsVars aty
@@ -314,44 +336,37 @@
       
       xNty = foldr (uncurry forall) (getBase n aty) (map fst perm)
       
-      sub = M.fromList [(x ,l), (x',l')]
+      sub = (x' |-> l') *** (x |-> l) -- M.fromList [(x , l), (x',l')]
 
-  modifyCtxt $ addToHead "-ggd-" Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!
-  
+  modifyCtxt $ addBefore "-ggd-" x Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!
+  modifyCtxt $ subst sub . removeFromContext x . removeFromContext x'
   vtrace 3 ("SUBST: -ggd- "++show sub) $ 
     return $ Just (sub, [] {- var xN :@: xNty] -}, False)
   
 gvar_uvar_inside a@(Spine _ yl, _) b@(Spine y _, _) = 
   case elemIndex (var y) $ reverse yl of
     Nothing -> return Nothing
-    Just _ -> gvar_uvar_outside a b
+    Just _ -> gvar_uvar_possibilities a b
 gvar_uvar_inside _ _ = error "gvar-uvar-inside is not made for this case"
-  
-gvar_const a@(s@(Spine x yl), _) b@(s'@(Spine y _), bty) = vtrace 3 (show a++"   ≐   "++show b) $
-  case elemIndex (var y) $ yl of 
-    Nothing -> gvar_fixed a b $ var . const y
-    Just _ -> do
-      gvar_uvar_outside a b <|> gvar_fixed a b (var . const y)
 
-gvar_const _ _ = error "gvar-const is not made for this case"
-
-gvar_uvar_outside a@(s@(Spine x yl),_) b@(s'@(Spine y _),bty) = do
-  let ilst = [i | (i,y') <- zip [0..] yl , y' == var y] 
-  i <- F.asum $ return <$> ilst
-  gvar_fixed a b $ (!! i) 
+gvar_uvar_outside = gvar_const
 
+gvar_const a@(s@(Spine x yl), _) b@(s'@(Spine y _), bty) = gvar_fixed a b $ var . const y
+gvar_const _ _ = error "gvar-const is not made for this case"
 
-gvar_uvar_outside _ _ = error "gvar-uvar-outside is not made for this case"
+gvar_uvar_possibilities a@(s@(Spine x yl),_) b@(s'@(Spine y _),bty) = 
+  case elemIndex (var y) yl of
+    Just i -> gvar_fixed a b $ (!! i)
+    Nothing -> throwTrace 0 $ "CANT: gvar-uvar-depends: "++show (s :=: s')
+gvar_uvar_possibilities _ _ = error "gvar-uvar-possibilities is not made for this case"
 
 getTyNews (Spine "#forall#" [_, Abs _ _ t]) = Nothing:getTyNews t
 getTyNews (Spine "#imp_forall#" [_, Abs nm _ t]) = Just nm:getTyNews t
 getTyNews _ = []
 
 gvar_fixed (a@(Spine x _), aty) (b@(Spine _ y'l), bty) action = do
-  let m = getTyNews bty -- max (length y'l) (getTyLen bty)
+  let m = getTyNews bty
       cons = a :=: b
---      getNewTys "@xm" bty 
-
   
   let getArgs (Spine "#forall#" [ty, Abs ui _ r]) = ((var ui,ui),Left ty):getArgs r
       getArgs (Spine "#imp_forall#" [ty, Abs ui _ r]) = ((tycon ui $ var ui,ui),Right ty):getArgs r
@@ -380,7 +395,8 @@
                            Left ty -> forall nm ty a
                            Right ty -> imp_forall nm ty a
                        ) e untylr
-
+                 
+      -- returns the list in the same order as xm
       substBty sub (Spine "#forall#" [_, Abs vi bi r]) ((x,xi):xmr) = (x,vbuild $ subst sub bi)
                                                                 :substBty (M.insert vi (fst xi) sub) r xmr
       substBty sub (Spine "#imp_forall#" [_, Abs vi bi r]) ((x,xi):xmr) = (x,vbuild $ subst sub bi)
@@ -391,14 +407,14 @@
                         ++ "\nON "++ show cons
       
       sub = x |-> l -- THIS IS THAT STRANGE BUG WHERE WE CAN'T use x in the output substitution!
-      addExists s t = vtrace 3 ("adding: "++show s++" ::: "++show t) $ addToHead "-gf-" Exists s t
-  modifyCtxt $ flip (foldr ($)) $ uncurry addExists <$> substBty mempty bty xm  
-  modifyCtxt $ subst sub
+      addExists s t = vtrace 3 ("adding: "++show s++" ::: "++show t) $ addAfter "-gf-" x Exists s t
+      -- foldr ($) addBeforeX [x1...xN]
+  modifyCtxt $ flip (foldr ($)) $ uncurry addExists <$> substBty mempty bty xm 
+  modifyCtxt $ subst sub . removeFromContext x
   vtrace 4 ("RES: -gg- "++(show $ subst sub $ a :=: b)) $ 
     vtrace 4 ("FROM: -gg- "++(show $ a :=: b)) $ 
     return $ Just (sub, [ subst sub $ a :=: b -- this ensures that the function resolves to the intended output
-                          
-                     ], False)
+                        ], False)
 
 gvar_fixed _ _ _ = error "gvar-fixed is not made for this case"
 
@@ -502,7 +518,7 @@
                     res <- Just <$> ls (nm,targ)
                     if sequ 
                       then (if not $ null cg then (appendErr "" (F.asum $ reverse cg) <|>) else id) $ 
-                           (appendErr "" $ ret res) <|> inter [] l
+                           (appendErr ""$ ret res) <|> inter [] l
                       else inter (ret res:cg) l
                       
                       
@@ -802,7 +818,7 @@
                   sub = subst $ nm' |-> ascribe val (dontcheck ty) 
           _ -> (l', resp:r, toplst)
 
-  (lst',l) <- inferAll (tys, [], topoSortAxioms lst)
+  (lst',l) <- inferAll (tys, [], topoSortAxioms True lst)
   
   let doubleCheckAll _ [] = return ()
       doubleCheckAll l (p:r) = do
@@ -820,22 +836,24 @@
                         ++ "\nunsound "++nm++" : "++show val
         doubleCheckAll (S.insert nm l) r
   
-  doubleCheckAll (S.union envSet uns) $ topoSortAxioms lst'
+  doubleCheckAll (S.union envSet uns) $ topoSortAxioms False lst' 
   
   return $ snd <$> l 
 
-
-topoSortAxioms :: [FlatPred] -> [FlatPred]
-topoSortAxioms axioms = topoSortComp (\p -> (p^.predName,) 
+topoSortAxioms :: Bool -> [FlatPred] -> [FlatPred]
+topoSortAxioms accountPot axioms = showRes $ topoSortComp (\p -> (p^.predName,) 
+                                            $ showGraph (p^.predName)
                                             -- unsound can mean this causes extra cyclical things to occur
-                                            $ (if p^.predSound then S.union (getImplieds $ p^.predName) else id)
+                                            $ (if accountPot && p^.predSound then S.union (getImplieds $ p^.predName) else id)
                                             $ S.fromList 
                                             $ concatMap (\nm -> [nm,"#v:"++nm])
                                             $ filter (not . flip elem (map fst consts)) 
                                             $ S.toList $ freeVariables p ) axioms
                         
-  where nm2familyLst  = catMaybes $ (\p -> (p^.predName,) <$> (p^.predFamily)) <$> axioms
+  where showRes a = vtrace 0 ("TOP_RESULT: "++show ((^.predName) <$> a)) a
+        showGraph n a = vtrace 1 ("TOP_EDGE: "++n++" -> "++show a) a
 
+        nm2familyLst  = catMaybes $ (\p -> (p^.predName,) <$> (p^.predFamily)) <$> axioms
         
         family2nmsMap = foldr (\(fam,nm) m -> M.insert nm (case M.lookup nm m of
                                   Nothing -> S.singleton fam
@@ -849,9 +867,19 @@
                                                   $ S.toList 
                                                   $ getImpliedFamilies 
                                                   $ p^.predType
-                                                 )) <$> axioms        
+                                                 )) <$> axioms
         
         getImplieds nm = fromMaybe mempty (M.lookup nm family2impliedsMap)
+
+getImpliedFamilies s = S.intersection fs $ gif s
+  where fs = freeVariables s
+        gif (Spine "#imp_forall#" [ty,a]) = (case getFamilyM ty of
+          Nothing -> id
+          Just f | f == atomName -> id
+          Just f -> S.insert f) $ gif ty `S.union` gif a 
+        gif (Spine a l) = mconcat $ gif <$> l
+        gif (Abs _ ty l) = S.union (gif ty) (gif l)
+
 
 typeCheckAll :: Bool -> [Decl] -> Choice [Decl]
 typeCheckAll verbose preds = do
diff --git a/Main.hs b/Main.hs
--- a/Main.hs
+++ b/Main.hs
@@ -64,6 +64,8 @@
 
 
 processFile :: Options -> IO ()
+processFile options | options ^. optHelp /= Nothing = case options ^. optHelp of
+  Just s -> putStrLn s
 processFile options = do
   let fname = options ^. optFile
       
diff --git a/Options.hs b/Options.hs
--- a/Options.hs
+++ b/Options.hs
@@ -3,6 +3,7 @@
  FlexibleContexts
  #-}
 module Options where
+import Data.List
 
 import Data.Maybe
 import Control.Lens (makeLenses, (.~))
@@ -12,13 +13,16 @@
                { _optIO_Only :: Bool
                , _optVerbose :: Int
                , _optFile :: String
-               } 
+               , _optHelp :: Maybe String
+               }
+               
 $(makeLenses ''Options)     
 
 defaultOptions = Options 
                { _optIO_Only  = False
                , _optVerbose  = 0
                , _optFile     = ""
+               , _optHelp     = Nothing
                }
 
 
@@ -32,21 +36,25 @@
     "a number describing how much debugging information to print"
   , Option ['f'] ["file", "infile", "input"]
     (ReqArg (optFile .~) "INFILE")
-    "the file to interpret and typecheck"
+    "a number describing how much debugging information to print"
+  , Option ['h'] ["help"]
+    (OptArg ((optHelp .~) . Just . fromMaybe helpMsg . fmap getMsg) "OPTION")
+    "display this help message"
   ]
 
 helpMessage = "Usage is \"caledon [--io-only] file.ncc\""
 
-arg_lst = [ ["--io-only", "-i"]
-          , ["--verbosity", "-V"]
-          , ["--help", "-h"]
-          , ["--file", "-f"]
-          ]
-  
 compilerOpts :: [String] -> IO (Options,[String])
 compilerOpts argv = 
   case getOpt Permute options argv of
     (o,n,[] ) -> return (foldl (flip id) defaultOptions o, n)
-    (_,_,errs) -> ioError $ userError $ concat errs ++ usageInfo header options
+    (_,_,errs) -> ioError $ userError $ concat errs ++ helpMsg
 
-header = "Usage: caledon [OPTIONS] file.ncc"
+helpMsg = usageInfo header options
+getMsg option = usageInfo header $ maybeToList 
+                $ find (\(Option s l _ _) -> elem option $ concat $ 
+                                         [[['-',i],[i]] | i <- s ] 
+                                       ++[["--"++i,i]   | i <- l ] 
+                       ) options
+  
+header = "Usage: caledon [OPTIONS] file.ncc" 
diff --git a/Substitution.hs b/Substitution.hs
--- a/Substitution.hs
+++ b/Substitution.hs
@@ -42,7 +42,7 @@
   return $ show n
   
 getNewWith :: (Functor f, MonadState c f, ValueTracker c) => String -> f String
-getNewWith s = {- (++s) <$> -} getNew
+getNewWith s = (++s) <$> getNew
 
                                
 ---------------------
@@ -103,15 +103,6 @@
 
 class Subst a where
   substFree :: Substitution -> S.Set Name -> a -> a
-  
-
-getImpliedFamilies s = S.intersection fs $ gif s
-  where fs = freeVariables s
-        gif (Spine "#imp_forall#" [ty,a]) = (case getFamilyM ty of
-          Nothing -> id
-          Just f -> S.insert f) $ gif ty `S.union` gif a 
-        gif (Spine a l) = mconcat $ gif <$> l
-        gif (Abs _ ty l) = S.union (gif ty) (gif l)
 
 subst :: Subst a => Substitution -> a -> a
 subst s = substFree s $ freeVariables s
diff --git a/caledon.cabal b/caledon.cabal
--- a/caledon.cabal
+++ b/caledon.cabal
@@ -1,6 +1,6 @@
 Name: caledon
 
-Version: 3.1.0.0
+Version: 3.2.0.0
 
 Description:         a dependently typed, polymorphic, higher order logic programming language based on the calculus of constructions designed for easier metaprogramming capabilities. 
 
diff --git a/examples/#test.ncc# b/examples/#test.ncc#
deleted file mode 100644
--- a/examples/#test.ncc#
+++ /dev/null
@@ -1,25 +0,0 @@
-#include "../prelude/prelude.ncc"
-
-query add0 = add (succ zero) zero (succ zero)
-
-query add1 = succ zero ++ zero == succ zero
-
-query add2 = exists A : natural . add (succ zero) zero A
-
-query add3 = any $ add (succ zero) zero
-
-query findSat1 = succ zero =< succ (succ zero)
-
-query findSat2 = succ zero =< succ (succ zero) /\ zero =< succ (succ zero)
-
-query findSat0 = free A : natural . A =:= zero
-
-
-defn ismain : prop 
-  as run $ do 
-         , putStr "hey!\n"
-         , readLine (\A . do 
-   	 , putStr A
-         , putStr "\nbye!\n")
-
-query main = ismain
diff --git a/examples/divergent.ncc b/examples/divergent.ncc
new file mode 100644
--- /dev/null
+++ b/examples/divergent.ncc
@@ -0,0 +1,10 @@
+defn unit : prop
+  >| u1 = unit
+
+defn divergent : unit -> prop
+   | divergentImp = divergent u1 -> divergent S
+
+
+defn moop : prop
+   | moopimp = moop <- divergent T
+query main = moop
diff --git a/examples/double.ncc b/examples/double.ncc
new file mode 100644
--- /dev/null
+++ b/examples/double.ncc
@@ -0,0 +1,15 @@
+fixity none 5 =:=
+defn =:= : char -> char -> prop
+   | eq = (B) =:= B
+
+defn char : prop
+
+defn putChar    :  char -> prop -- builtin
+   | putCharImp = [A : char] putChar A
+
+defn main : prop
+   | mainImp = main 
+               <- S =:= 'h'
+               <- putChar S
+
+query main1 = main
diff --git a/examples/listTest.ncc b/examples/listTest.ncc
new file mode 100644
--- /dev/null
+++ b/examples/listTest.ncc
@@ -0,0 +1,11 @@
+----------------
+--- Booleans ---
+----------------
+defn bool : prop
+   | true = bool
+   | false = bool
+
+fixity none 0 ==>
+defn ==> : {A : prop} bool -> ((A -> A -> A) -> A) -> A -> prop
+   | thentrue  = [F] (true ==> F ) (F (\a1 a2 : A . a1) )
+   | thenfalse = [F] (false ==> F) (F (\a1 a2 : B . a2))
diff --git a/examples/tactics.ncc b/examples/tactics.ncc
new file mode 100644
--- /dev/null
+++ b/examples/tactics.ncc
@@ -0,0 +1,23 @@
+#include "../prelude/logic.ncc"
+
+-- just because we can define the theorem 
+-- doesn't mean we can prove it (we don't have switch?)
+
+defn natural : prop
+  as ∀ a : prop . a → (a → a)  → a
+
+defn zero : natural
+  as λ a : prop . λ z : a . λ s : a → a . z
+
+defn succ : natural → natural
+  as λ n : natural . λ a : prop . λ z : a . λ s : a → a . s (n a z s)
+
+defn even : natural → prop
+   | even-zero = even zero
+   | even-succ = [A : natural] even A -> even (succ (succ A))
+
+defn add : natural → natural → natural
+  as λ n₁ n₂ : natural . n₁ natural n₂ succ
+
+defn thm : prop
+  as ∀ N . even (add N N)
diff --git a/prelude/booleans.ncc b/prelude/booleans.ncc
--- a/prelude/booleans.ncc
+++ b/prelude/booleans.ncc
@@ -2,8 +2,8 @@
 --- Booleans ---
 ----------------
 defn bool : prop
-  >| true = bool
-  >| false = bool
+   | true = bool
+   | false = bool
 
 defn if : bool -> bool
   as \b . b
@@ -15,8 +15,8 @@
 
 fixity none 0 ==>
 defn ==> : {A : prop} bool -> ((A -> A -> A) -> A) -> A -> prop
-  >| thentrue  = [F: _ -> A] (true ==> F ) (F (\a1 a2 : A . a1) )
-  >| thenfalse = [F: _ -> B] (false ==> F) (F (\a1 a2 : B . a2))
+  >| thentrue  = (true  ==> F) (F (\a1 a2 : A . a1) )
+  >| thenfalse = (false ==> F) (F (\a1 a2 : B . a2))
 
 defn not : bool -> bool -> prop
   as \zq . if zq ==> false |:| true
diff --git a/prelude/list.ncc b/prelude/list.ncc
--- a/prelude/list.ncc
+++ b/prelude/list.ncc
@@ -2,8 +2,8 @@
 --- Lists ---
 -------------
 defn list : prop -> prop
-  >| nil  = list A
-  >| cons = A -> list A -> list A
+   | nil  = list A
+   | cons = A -> list A -> list A
 
 defn concatList : list A -> list A -> list A -> prop
   >| concatListNil  = concatList {A = T} nil L L
diff --git a/prelude/naturals.ncc b/prelude/naturals.ncc
--- a/prelude/naturals.ncc
+++ b/prelude/naturals.ncc
@@ -3,8 +3,8 @@
 ---------------------
 
 defn natural  : prop
-  >| zero = natural
-  >| succ = natural -> natural
+   | zero = natural
+   | succ = natural -> natural
 
 defn add   : natural -> natural -> natural -> prop
   >| add_z = add zero N N