diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal
--- a/liquid-fixpoint.cabal
+++ b/liquid-fixpoint.cabal
@@ -1,5 +1,5 @@
 name:                liquid-fixpoint
-version:             0.7.0.6
+version:             0.7.0.7
 Copyright:           2010-17 Ranjit Jhala, University of California, San Diego.
 synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 homepage:            https://github.com/ucsd-progsys/liquid-fixpoint
diff --git a/src/Language/Fixpoint/Solver/Instantiate.hs b/src/Language/Fixpoint/Solver/Instantiate.hs
--- a/src/Language/Fixpoint/Solver/Instantiate.hs
+++ b/src/Language/Fixpoint/Solver/Instantiate.hs
@@ -65,7 +65,7 @@
   where
     (is, ps)         = unzip ips
     (ps', axs)       = defuncAxioms cfg env ps
-    ps''             = elaborate "PLE1" env <$> ps'
+    ps''             = zipWith (\i -> elaborate ("PLE1 " ++ show i) env) is ps' -- <$> ps'
     axs'             = elaborate "PLE2" env <$> axs
     fi'              = fi { asserts = axs' ++ asserts fi }
 
@@ -416,40 +416,24 @@
 substEqCoerce eq es bd = do
   env      <- seSort <$> gets evEnv
   let ts    = snd    <$> eqArgs eq
-  let coSub = mkCoSub env es ts
-  return    $ applyCoSub coSub bd
-
--- | @CoSub@ is a map from (coercion) ty-vars represented as 'FObj s'
---   to the ty-vars that they should be substituted with. Note the
---   domain and range are both Symbol and not the Int used for real ty-vars.
-
-type CoSub = M.HashMap Symbol Symbol
+  let sp    = panicSpan "mkCoSub"
+  let eTs   = sortExpr sp env <$> es
+  let coSub = notracepp ("substEqCoerce" ++ showpp (eqName eq, es, eTs, ts)) $ mkCoSub eTs ts
+  return    $ Vis.applyCoSub coSub bd
 
-mkCoSub :: SEnv Sort -> [Expr] -> [Sort] -> CoSub
-mkCoSub env es xTs = Misc.safeFromList "mkCoSub" xys
+mkCoSub :: [Sort] -> [Sort] -> Vis.CoSub
+mkCoSub eTs xTs = Misc.safeFromList "mkCoSub" xys
   where
-    eTs            = sortExpr sp env <$> es
-    sp             = panicSpan "mkCoSub"
-    xys            = concat (zipWith matchSorts xTs eTs)
+    xys         = concat (zipWith matchSorts xTs eTs)
 
-matchSorts :: Sort -> Sort -> [(Symbol, Symbol)]
-matchSorts = go
+matchSorts :: Sort -> Sort -> [(Symbol, Sort)]
+matchSorts s1 s2 = notracepp ("matchSorts :" ++ show (s1, s2)) $ go s1 s2
   where
-    go (FObj x)      (FObj y)      = [(x, y)]
+    go (FObj x)      {-FObj-} y    = [(x, y)]
     go (FAbs _ t1)   (FAbs _ t2)   = go t1 t2
     go (FFunc s1 t1) (FFunc s2 t2) = go s1 s2 ++ go t1 t2
     go (FApp s1 t1)  (FApp s2 t2)  = go s1 s2 ++ go t1 t2
     go _             _             = []
-
-applyCoSub :: CoSub -> Expr -> Expr
-applyCoSub coSub      = Vis.mapExpr fE
-  where
-    fE (ECoerc s t e) = ECoerc (txS s) (txS t) e
-    fE e              = e
-    txS               = Vis.mapSort fS
-    fS (FObj a)       = FObj   (txV a)
-    fS t              = t
-    txV a             = M.lookupDefault a a coSub
 
 --------------------------------------------------------------------------------
 getEqBody :: Equation -> Maybe Expr
diff --git a/src/Language/Fixpoint/SortCheck.hs b/src/Language/Fixpoint/SortCheck.hs
--- a/src/Language/Fixpoint/SortCheck.hs
+++ b/src/Language/Fixpoint/SortCheck.hs
@@ -450,13 +450,13 @@
   ps' <- mapM (elab f) ps
   return (POr (fst <$> ps'), boolSort)
 
-elab f@(_,g) e@(PAtom Eq e1 e2) = do
+elab f@(_,g) e@(PAtom eq e1 e2) | eq == Eq || eq == Ne = do
   t1        <- checkExpr g e1
   t2        <- checkExpr g e2
   (t1',t2') <- unite g e  t1 t2 `withError` (errElabExpr e)
   e1'       <- elabAs f t1' e1
   e2'       <- elabAs f t2' e2
-  return (PAtom Eq (ECst e1' t1') (ECst e2' t2') , boolSort)
+  return (PAtom eq (ECst e1' t1') (ECst e2' t2') , boolSort)
 
 elab f (PAtom r e1 e2)
   | r == Ueq || r == Une = do
diff --git a/src/Language/Fixpoint/Types/Names.hs b/src/Language/Fixpoint/Types/Names.hs
--- a/src/Language/Fixpoint/Types/Names.hs
+++ b/src/Language/Fixpoint/Types/Names.hs
@@ -240,7 +240,7 @@
 type LocText   = Located T.Text
 
 isDummy :: (Symbolic a) => a -> Bool
-isDummy a = symbol a == symbol dummyName
+isDummy a = isPrefixOfSym (symbol dummyName) (symbol a)
 
 instance Symbolic a => Symbolic (Located a) where
   symbol = symbol . val
diff --git a/src/Language/Fixpoint/Types/Visitor.hs b/src/Language/Fixpoint/Types/Visitor.hs
--- a/src/Language/Fixpoint/Types/Visitor.hs
+++ b/src/Language/Fixpoint/Types/Visitor.hs
@@ -33,6 +33,10 @@
   , mapKVars, mapKVars', mapGVars', mapKVarSubsts
   , mapExpr, mapMExpr
 
+  -- * Coercion Substitutions
+  , CoSub
+  , applyCoSub
+
   -- * Predicates on Constraints
   , isConcC , isKvarC
 
@@ -318,6 +322,25 @@
 --  where
 --    go (ECst e _) = e
 --    go e          = e
+
+--------------------------------------------------------------------------------
+-- | @CoSub@ is a map from (coercion) ty-vars represented as 'FObj s'
+--   to the ty-vars that they should be substituted with. Note the
+--   domain and range are both Symbol and not the Int used for real ty-vars.
+--------------------------------------------------------------------------------
+
+type CoSub = M.HashMap Symbol Sort -- Symbol
+
+applyCoSub :: CoSub -> Expr -> Expr
+applyCoSub coSub      = mapExpr fE
+  where
+    fE (ECoerc s t e) = ECoerc  (txS s) (txS t) e
+    fE (ELam (x,t) e) = ELam (x, txS t)         e
+    fE e              = e
+    txS               = mapSort fS
+    fS (FObj a)       = {- FObj -} (txV a)
+    fS t              = t
+    txV a             = M.lookupDefault (FObj a) a coSub
 
 ---------------------------------------------------------------------------------
 -- | Visitors over @Sort@