diff --git a/Src/ChkRaw.hs b/Src/ChkRaw.hs
index 9d53e8c..e519f79 100644
--- a/Src/ChkRaw.hs
+++ b/Src/ChkRaw.hs
@@ -431,9 +431,11 @@ fromSubs g f = hnf f >>= \case
       (_, _, TE (TP (xn, _))) ->
            fred $ PROVE (e4p (xn, lhs ::: ty) g)
       _ -> fred . GIVEN q $ PROVE g
-  f -> map snd {- ignorant -} <$> invert f >>= \case
-    [[s]] -> flop s g
-    rs -> mapM_ (fred . foldr (GIVEN . propify) (PROVE g)) rs
+  f -> invert f >>= \case
+    [([], [s])] -> flop s g
+    rs -> mapM_
+      (\ (de, hs) -> fred . disch de $ foldr (GIVEN . propify) (PROVE g) hs)
+      rs
  where
   flop (PROVE p)   g = fred . GIVEN p $ PROVE g
   flop (GIVEN h s) g = do
@@ -441,6 +443,15 @@ fromSubs g f = hnf f >>= \case
     flop s g
   propify (GIVEN s t) = s :-> propify t
   propify (PROVE p)   = p
+  disch [] g = g
+  disch (Bind (xn, Hide s) _ : hs) g =
+    EVERY s (xn \\ disch hs g)
+  disch (Hyp _ h : hs) g = GIVEN h $
+    let g' = disch hs g in case h of
+      TC "=" [ty, TE (TP (xn, _)), t] | not (pDep xn t) ->
+        e4p (xn, t ::: ty) g'
+      _ -> g'
+  disch (_ : hs) g = disch hs g
 
 ginger :: Bwd Tm -> [(Tm, (Tm, Tm))] -> Tm -> AM ()
 ginger qz [] g = fred $ foldr GIVEN (PROVE g) qz
@@ -861,52 +872,3 @@ filthier as s = case runAM go () as of
     let (fo, b) = raw fi s
     setFixities fo
     bifoldMap (($ "") . rfold lout) id <$> traverse askRawDecl b
-
-foo = unlines
-  [ "data List x = Empty | x : List x"
-  , "(++) :: List x -> List x -> List x"
-  , "define xs ++ ys inductively xs where"
-  , "  define xs ++ ys from xs where"
-  , "    define Empty ++ ys = ys"
-  , "    define (x : xs') ++ ys = x : (xs' ++ ys)"
-  , "prove xs ++ Empty = xs inductively xs where"
-  , "  prove xs ++ Empty = xs from xs where"
-  , "    given xs = x : xs' prove (x : xs') ++ Empty = x : xs' tested"
-  ]
-
-goo = unlines
-  [ "data Tree = Leaf | Node Tree Tree"
-  , "mirror :: Tree -> Tree"
-  , "define mirror t inductively t where"
-  , "  define mirror t from t where"
-  , "    define mirror Leaf = Leaf"
-  , "    define mirror (Node l r) = Node (mirror r) (mirror l)"
-  , "prove mirror (mirror t) = t inductively t where"
-  , "  prove mirror (mirror t) = t from t where"
-  , "    given t = Node l r prove mirror (mirror (Node l r)) = Node l r tested"
-  ]
-
-hoo = unlines
-  [ "data List x = Empty | x : List x"
-  , "(++) :: List x -> List x -> List x"
-  , "define xs ++ ys inductively xs where"
-  , "  define xs ++ ys from xs where"
-  , "    define Empty ++ ys = ys"
-  , "    define (x : xs') ++ ys = x : (xs' ++ ys)"
-  , "prove (xs ++ ys) ++ zs = xs ++ (ys ++ zs) inductively xs where"
-  , "  prove (xs ++ ys) ++ zs = xs ++ (ys ++ zs) from xs where"
-  , "    given xs = x : xs' prove ((x : xs') ++ ys) ++ zs = (x : xs') ++ (ys ++ zs) tested"
-  ]
-
-ioo = unlines
-  [ "data N = Z | S N"
-  , "(+) :: N -> N -> N"
-  , "defined x + y inductively x where"
-  , "  defined x + y from x where"
-  , "    defined Z + y = y"
-  , "    defined S x + y = S (x + y)"
-  , "prove (x + y) + z = x + (y + z) inductively x where"
-  , "  prove (x + y) + z = x + (y + z) from x where"
-  , "    given x = S x' prove (S x' + y) + z = S x' + (y + z)"
-  , "      tested"
-  ]
\ No newline at end of file
diff --git a/Src/HardwiredRules.hs b/Src/HardwiredRules.hs
index e04c813..ae3c22b 100644
--- a/Src/HardwiredRules.hs
+++ b/Src/HardwiredRules.hs
@@ -60,6 +60,14 @@ myWeirdRules =
     [ PROVE $ TC "=" [TM "T" [], TM "r" [], TM "s" []]
     , PROVE $ TC "=" [TM "T" [], TM "s" [], TM "t" []]
     ]
+  , (PC "=" [PC "->" [PM "S" mempty, PM "T" mempty], PM "f" mempty, PM "g" mempty],
+     ("Applying", Pr [])) :<=
+    [ EVERY (TM "S" []) . L . PROVE $ TC "="
+       [ TM "T" []
+       , TE ((TM "f" mempty ::: TC "->" [TM "S" mempty, TM "T" mempty]) :$ TE (TV 0))
+       , TE ((TM "g" mempty ::: TC "->" [TM "S" mempty, TM "T" mempty]) :$ TE (TV 0))
+       ]
+    ]
   ]
 
 myContext :: Context
diff --git a/Src/Proving.hs b/Src/Proving.hs
index 4a8ee19..b5ebce8 100644
--- a/Src/Proving.hs
+++ b/Src/Proving.hs
@@ -11,7 +11,9 @@
 module Ask.Src.Proving where
 
 import Data.Foldable
+import Data.Traversable
 
+import Ask.Src.Thin
 import Ask.Src.Hide
 import Ask.Src.Bwd
 import Ask.Src.Lexing
@@ -47,15 +49,106 @@ by goal a@(_, (t, _, r) :$$ ss) | elem t [Uid, Sym] = do
   backchain _ = return []
 by goal r = gripe $ NotARule r
 
-invert :: Tm -> AM [((String, Tel), [Subgoal])]
+invert :: Tm -> AM [([CxE], [Subgoal])]
 invert hyp = fold <$> (gamma >>= traverse try )
  where
-  try :: CxE -> AM [((String, Tel), [Subgoal])]
-  try (ByRule True ((gop, (h, tel)) :<= prems)) = cope (maAM (gop, hyp))
-    (\ _ -> return [])
-    (\ m -> return [((h, stan m tel), stan m prems)])
+  try :: CxE -> AM [([CxE], [Subgoal])]
+  try (ByRule True ((gop, (h, tel)) :<= prems)) = do
+    doorStop
+    m <- prayTel [] tel
+    True <- trice ("INVERT TRIES: " ++ show ((hyp, gop), (h, tel), prems)) $ return True
+    gingerly m Prop gop hyp >>= \case
+      [(_, m)] -> do
+        let prems' = stan m prems
+        de <- doorStep
+        True <- trice ("INVERT: " ++ show m ++ " ===> " ++
+                  show (de, prems')) $ return True
+        return [(de, prems')]
+      _ -> doorStep *> return []
   try _ = return []
 
+prayTel :: Matching -> Tel -> AM Matching
+prayTel m (Pr hs) = do
+  for (stan m hs) $ \ h -> push $ Hyp True h
+  return m
+prayTel m (Ex s b) = do
+  xn <- fresh "x"
+  let u = "x" ++ show (snd (last xn)) -- BOO!
+  let xp = (xn, Hide (stan m s))
+  push $ Bind xp (User u)
+  prayTel m (b // TP xp)
+prayTel m ((x, s) :*: t) = do
+  xn <- fresh x
+  let u = x ++ show (snd (last xn)) -- BOO!
+  let xp = (xn, Hide (stan m s))
+  push $ Bind xp (User u)
+  prayTel ((x, TE (TP xp)) : m) t
+
+prayPat :: Matching -> Tm -> Pat -> AM (Syn, Matching)
+prayPat m ty (PC c ps) = do
+  ty <- hnf $ stan m ty
+  tel <- constructor PAT ty c
+  (ts, m) <- prayPats m tel ps
+  return (TC c ts ::: ty, m)
+prayPat m ty (PM x _) = do
+  xn <- fresh x
+  let u = "x" ++ show (snd (last xn)) -- BOO!
+  let xp = (xn, Hide (stan m ty))
+  push $ Bind xp (User u)
+  return (TP xp, (x, TE (TP xp)) : m)
+
+prayPats :: Matching -> Tel -> [Pat] -> AM ([Tm], Matching)
+prayPats m (Pr hs) [] = do
+  for (stan m hs) $ \ h -> push $ Hyp True h
+  return ([], m)
+prayPats m (Ex s b) (p : ps) = do
+  (e, m) <- prayPat m s p
+  (ts, m) <- prayPats m (b // e) ps
+  return (upTE e : ts, m)
+prayPats m ((x, s) :*: tel) (p : ps) = do
+  (e, m) <- prayPat m s p
+  (ts, m) <- prayPats ((x, upTE e) : m) tel ps
+  return (upTE e : ts, m)
+prayPats _ _ _ = gripe Mardiness
+
+gingerly :: Matching -> Tm -> Pat -> Tm -> AM [(Syn, Matching)]
+gingerly m ty p@(PC gc ps) t = hnf t >>= \case
+  TC hc ts | gc /= hc -> return [] | otherwise -> do
+    let ty' = stan m ty
+    tel <- constructor PAT ty' gc
+    gingerlies m tel ps ts >>= \case
+      [(us, m)] -> return [(TC gc us ::: ty', m)]
+      _ -> return []
+  t -> do
+    let ty' = case t of
+          TE (TP (_, Hide ty)) -> ty -- would like a size if it's there
+          _ -> ty
+    (e, m) <- prayPat m ty' p
+    push . Hyp True $ TC "=" [ty', t, upTE e]
+    return [(e, m)]
+gingerly m ty (PM x th) t = case trice ("GINGERLY PM: " ++ x) $ thicken th t of
+  Nothing -> return []
+  Just u -> return [(t ::: stan m ty, (x, u) : m)]
+gingerly _ _ _ _ = gripe Mardiness
+
+
+gingerlies :: Matching -> Tel -> [Pat] -> [Tm] -> AM [([Tm], Matching)]
+gingerlies m (Pr hs) [] [] = do
+  for (stan m hs) $ \ h -> push $ Hyp True h
+  return [([], m)]
+gingerlies m (Ex s b) (p : ps) (t : ts) = gingerly m s p t >>= \case
+  [(e, m)] -> gingerlies m (b // e) ps ts >>= \case
+    [(us, m)] -> return [(upTE e : us, m)]
+    _ -> return []
+  _ -> return []
+gingerlies m ((x, s) :*: tel) (p : ps) (t : ts) = gingerly m s p t >>= \case
+  [(e, m)] -> let u = upTE e in
+    gingerlies ((x, u) : m) tel ps ts >>= \case
+      [(us, m)] -> return [(u : us, m)]
+      _ -> return []
+  _ -> return []
+gingerlies _ _ _ _ = return []
+
 given :: Tm -> AM Bool{-proven?-}
 given goal = do
   ga <- gamma
diff --git a/Src/Typing.hs b/Src/Typing.hs
index dc1d27f..5962e99 100644
--- a/Src/Typing.hs
+++ b/Src/Typing.hs
@@ -572,13 +572,11 @@ make xp@(x, Hide ty) t got = do
     True <- track ("AWOL " ++ show x) $ return True
     gripe FAIL -- shouldn't happen
   go (ga :< z) ms | track ("MAKE-GO: " ++ show z ++ " " ++ show ms) False = undefined
-  go (ga :< Bind p@(y, _) Hole) ms | x == y = do
-    pDep y (ms, t) >>= \case
+  go (ga :< Bind p@(y, _) Hole) ms | x == y = case pDep y (ms, t) of
       True -> gripe FAIL
       False -> return (ga <>< ms :< Bind p (Defn t))
   go (ga :< Bind (y, _) _) ms | x == y = gripe FAIL
-  go (ga :< z@(Bind (y, _) k)) ms = do
-    pDep y (ms, t) >>= \case
+  go (ga :< z@(Bind (y, _) k)) ms = case pDep y (ms, t) of
       False -> (:< z) <$> go ga ms
       True -> case k of
         User _ -> gripe FAIL
@@ -591,28 +589,26 @@ make xp@(x, Hide ty) t got = do
 ------------------------------------------------------------------------------
 
 class PDep t where
-  pDep :: Nom -> t -> AM Bool
+  pDep :: Nom -> t -> Bool
 
 instance PDep Tm where
-  pDep x t = case t of {- do
-    hnf t >>= \case -}
+  pDep x t = case t of
       TC _ ts -> pDep x ts
       TB t -> pDep x t
       TE e -> pDep x e
 
 instance PDep Syn where
-  pDep x (TP (y, _)) = return $ x == y
-  pDep x (t ::: ty) = (||) <$> pDep x t <*> pDep x ty
-  pDep x (e :$ s) =  (||) <$> pDep x e <*> pDep x s
-  pDep x (TF _ is as) = (||) <$> pDep x is <*> pDep x as
-  pDep x _ = return False
+  pDep x (TP (y, _)) =  x == y
+  pDep x (t ::: ty) = pDep x t || pDep x ty
+  pDep x (e :$ s) =  pDep x e || pDep x s
+  pDep x (TF _ is as) = pDep x is || pDep x as
+  pDep x _ = False
 
 instance PDep t => PDep [t] where
-  pDep x ts = do
-    any id <$> traverse (pDep x) ts
+  pDep x ts = any id (map (pDep x) ts)
 
 instance (PDep s, PDep t) => PDep (s, t) where
-  pDep x (s, t) = (||) <$> pDep x s <*> pDep x t
+  pDep x (s, t) = pDep x s || pDep x t
 
 instance PDep t => PDep (Bind t) where
   pDep x (K t) = pDep x t
@@ -620,12 +616,12 @@ instance PDep t => PDep (Bind t) where
 
 instance PDep CxE where
   pDep x (Hyp _ p) = pDep x p
-  pDep x (Bind (_, Hide ty) k) = (||) <$> pDep x ty <*> pDep x k
-  pDep _ _ = return False
+  pDep x (Bind (_, Hide ty) k) = pDep x ty || pDep x k
+  pDep _ _ = False
 
 instance PDep BKind where
   pDep x (Defn t) = pDep x t
-  pDep _ _ = return False
+  pDep _ _ = False
 
 
 ------------------------------------------------------------------------------
@@ -664,7 +660,7 @@ telify vs lox = go [] lox where
   go ps (Bind (xp, Hide ty) bk : lox) = case bk of
     Defn t -> e4p (xp, t ::: ty) <$> go ps lox
     Hole -> do
-      bs <- traverse (\ (_, (xp, _)) -> pDep xp ty) ps
+      bs <- traverse (\ (_, (xp, _)) -> return $ pDep xp ty) ps
       guard $ all not bs
       Ex ty <$> ((xp \\) <$> go ps lox)
     User x -> e4p (xp, TM x [] ::: ty) <$> go ((x, (xp, ty)) : ps) lox
@@ -682,14 +678,14 @@ schemify vs lox rt = go [] lox where
   go ps (Bind (xp, Hide ty) bk : lox) = case bk of
     Defn t -> e4p (xp, t ::: ty) <$> go ps lox
     Hole -> do
-      bs <- traverse (\ (_, (xp, _)) -> pDep xp ty) ps
+      bs <- traverse (\ (_, (xp, _)) -> return $ pDep xp ty) ps
       guard $ all not bs
       Al ty <$> ((xp \\) <$> go ps lox)
     User x
       | x `elem` vs ->
         e4p (xp, TM x [] ::: ty) <$> go ((x, (xp, ty)) : ps) lox
       | otherwise -> do
-        bs <- traverse (\ (_, (xp, _)) -> pDep xp ty) ps
+        bs <- traverse (\ (_, (xp, _)) -> return $ pDep xp ty) ps
         guard $ all not bs
         Al ty <$> ((xp \\) <$> go ps lox)
   go ps ((_ ::> _) : lox) = go ps lox