diff --git a/nova.ipkg b/nova.ipkg
index c799b9e..d54980f 100644
--- a/nova.ipkg
+++ b/nova.ipkg
@@ -35,8 +35,8 @@ modules =
         , Nova.Surface.SemanticToken
         , Nova.Surface.Shunting
 
-        , Nova.Surface.Tactic.Reduce
         , Nova.Surface.Tactic.Trivial
+        , Nova.Surface.Tactic.Unfold
 
         , Nova.Test.Test
 
diff --git a/src/idris/Nova/Surface/Elaboration.idr b/src/idris/Nova/Surface/Elaboration.idr
index 5511643..d9a19a3 100644
--- a/src/idris/Nova/Surface/Elaboration.idr
+++ b/src/idris/Nova/Surface/Elaboration.idr
@@ -28,7 +28,7 @@ import Nova.Surface.Shunting
 import Nova.Surface.Operator
 import Nova.Surface.SemanticToken
 
-import Nova.Surface.Tactic.Reduce
+import Nova.Surface.Tactic.Unfold
 import Nova.Surface.Tactic.Trivial
 
 CoreTyp = Nova.Core.Language.D.Typ
@@ -1296,13 +1296,13 @@ mutual
     Right (omega, source, restInterp) <- elabTactic sig omega (Composition r (beta ::: gammas)) alphaSource
       | Left err => return (Left err)
     return (Right (omega, source, restInterp . alphaInterp))
-  -- ⟦reduce ρ⟧ : ε (Γ ⊦ B) ⇒ ε (Γ ⊦ A)
-  elabTactic sig omega (Reduce r path) [< (x, ElemEntry ctx ty)] = M.do
-   Right ty' <- Elab.liftM $ applyReduce sig omega ty path
+  -- ⟦unfold ρ⟧ : ε (Γ ⊦ B) ⇒ ε (Γ ⊦ A)
+  elabTactic sig omega (Unfold r path) [< (x, ElemEntry ctx ty)] = M.do
+   Right ty' <- Elab.liftM $ applyUnfold sig omega (map fst ctx) ty path
      | Left r => --FIX: use the range
-                 return (Left "Can't apply 'reduce', range: \{show r}, ρ: \{show path}")
+                 return (Left "Can't apply 'unfold', range: \{show r}, ρ: \{show path}")
    return (Right (omega, [< (x, ElemEntry ctx ty')], id))
-  elabTactic sig omega (Reduce r path) _ = return (Left "Target context is empty or its last entry is a let")
+  elabTactic sig omega (Unfold r path) _ = return (Left "Target context is empty or its last entry is a let")
   elabTactic sig omega (RewriteInv r path prf) [< (x, ElemEntry ctx ty)] = M.do
     case !(applyRewrite sig omega ctx ty path prf False) of
       Left r0 => M.do
diff --git a/src/idris/Nova/Surface/Language.idr b/src/idris/Nova/Surface/Language.idr
index e5f343f..210f318 100644
--- a/src/idris/Nova/Surface/Language.idr
+++ b/src/idris/Nova/Surface/Language.idr
@@ -113,8 +113,8 @@ mutual
       ||| α
       ||| β
       Composition : Range -> List1 Tactic -> Tactic
-      ||| reduce ρ
-      Reduce : Range -> Term -> Tactic
+      ||| unfold ρ
+      Unfold : Range -> Term -> Tactic
       ||| exact t
       Exact : Range -> Term -> Tactic
       ||| * α
@@ -138,8 +138,8 @@ mutual
       ||| α
       ||| β
       Composition : Range -> List1 OpFreeTactic -> OpFreeTactic
-      ||| reduce ρ
-      Reduce : Range -> OpFreeTerm -> OpFreeTactic
+      ||| unfold ρ
+      Unfold : Range -> OpFreeTerm -> OpFreeTactic
       ||| exact t
       Exact : Range -> OpFreeTerm -> OpFreeTactic
       ||| * α
diff --git a/src/idris/Nova/Surface/Parser.idr b/src/idris/Nova/Surface/Parser.idr
index 7e6f8b9..13e9b8a 100644
--- a/src/idris/Nova/Surface/Parser.idr
+++ b/src/idris/Nova/Surface/Parser.idr
@@ -619,11 +619,11 @@ mutual
     sepBy1 spaceDelimDef topLevel
 
 mutual
-  tactic = composition <|> split <|> exact <|> reduce <|> id <|> trivial <|> rewriteInv <|> let' <|> rewrite'
+  tactic = composition <|> split <|> exact <|> unfold <|> id <|> trivial <|> rewriteInv <|> let' <|> rewrite'
 
   public export
   compositionArg : Rule Tactic
-  compositionArg = split <|> exact <|> reduce <|> id <|> trivial <|> rewriteInv <|> let' <|> rewrite'
+  compositionArg = split <|> exact <|> unfold <|> id <|> trivial <|> rewriteInv <|> let' <|> rewrite'
 
   ensureColumn : (col : Int) -> Rule a -> Rule a
   ensureColumn col f = do
@@ -660,12 +660,12 @@ mutual
     pure (Exact (l + r) tm)
 
   public export
-  reduce : Rule Tactic
-  reduce = do
-    l <- delim "reduce"
+  unfold : Rule Tactic
+  unfold = do
+    l <- delim "unfold"
     spaceDelim
     (r, tm) <- located (term 0)
-    pure (Reduce (l + r) tm)
+    pure (Unfold (l + r) tm)
 
   continueSplit : (col : Int) -> Rule (List Tactic)
   continueSplit col = do
diff --git a/src/idris/Nova/Surface/Shunting.idr b/src/idris/Nova/Surface/Shunting.idr
index 5e8855a..eada86c 100644
--- a/src/idris/Nova/Surface/Shunting.idr
+++ b/src/idris/Nova/Surface/Shunting.idr
@@ -181,9 +181,9 @@ mutual
   shuntTactic ops (Composition r alphas) = MEither.do
     alphas <- forList1 alphas (shuntTactic ops)
     return (Composition r alphas)
-  shuntTactic ops (Reduce r tm) = MEither.do
+  shuntTactic ops (Unfold r tm) = MEither.do
     tm <- shunt ops tm 0
-    return (Reduce r tm)
+    return (Unfold r tm)
   shuntTactic ops (Exact r tm) = MEither.do
     tm <- shunt ops tm 0
     return (Exact r tm)
diff --git a/src/idris/Nova/Surface/Tactic/Reduce.idr b/src/idris/Nova/Surface/Tactic/Reduce.idr
deleted file mode 100644
index d0a5346..0000000
--- a/src/idris/Nova/Surface/Tactic/Reduce.idr
+++ /dev/null
@@ -1,246 +0,0 @@
-module Nova.Surface.Tactic.Reduce
-
-import Data.Location
-import Data.SnocList
-
-import Nova.Core.Context
-import Nova.Core.Language
-import Nova.Core.Monad
-import Nova.Core.Evaluation
-
-import Nova.Surface.Language
-
--- This module contains support code for the reduce tactic
-
-mutual
-  namespace Typ
-    ||| Try applying reduce tactic on a well-typed term
-    ||| Γ ⊦ t : T
-    ||| or
-    ||| Γ ⊦ T type
-    ||| The term must be head-neutral w.r.t. open evaluation
-    ||| OpFreeTerm must represent a valid path!
-    ||| See Surface/Language for a description of being a valid path.
-    public export
-    applyReduceNu : Signature -> Omega -> Typ -> OpFreeTerm -> M (Either Range Typ)
-    applyReduceNu sig omega el (App _ (Tm _ tm) []) = MEither.do
-      applyReduce sig omega el tm
-    applyReduceNu sig omega (El el) path = MEither.do
-      return $ El !(applyReduce sig omega el path)
-    applyReduceNu sig omega (PiTy x dom cod) (PiTy r _ pdom (App _ (Underscore _) [])) = MEither.do
-      return $ PiTy x !(applyReduce sig omega dom pdom) cod
-    applyReduceNu sig omega (PiTy x dom cod) (FunTy r pdom (App _ (Underscore _) [])) = MEither.do
-      return $ PiTy x !(applyReduce sig omega dom pdom) cod
-    applyReduceNu sig omega (PiTy x dom cod) (PiTy r _ (App _ (Underscore _) []) pcod) = MEither.do
-      return $ PiTy x dom !(applyReduce sig omega cod pcod)
-    applyReduceNu sig omega (PiTy x dom cod) (FunTy r (App _ (Underscore _) []) pcod) = MEither.do
-      return $ PiTy x dom !(applyReduce sig omega cod pcod)
-    applyReduceNu sig omega (PiTy x dom cod) p = error (range p)
-    applyReduceNu sig omega (ImplicitPiTy x dom cod) (ImplicitPiTy r _ pdom (App _ (Underscore _) [])) = MEither.do
-      return $ ImplicitPiTy x !(applyReduce sig omega dom pdom) cod
-    applyReduceNu sig omega (ImplicitPiTy x dom cod) (ImplicitPiTy r _ (App _ (Underscore _) []) pcod) = MEither.do
-      return $ ImplicitPiTy x dom !(applyReduce sig omega cod pcod)
-    applyReduceNu sig omega (ImplicitPiTy x dom cod) p = error (range p)
-    applyReduceNu sig omega (SigmaTy x dom cod) (SigmaTy r _ pdom (App _ (Underscore _) [])) = MEither.do
-      return $ SigmaTy x !(applyReduce sig omega dom pdom) cod
-    applyReduceNu sig omega (SigmaTy x dom cod) (SigmaTy r _ (App _ (Underscore _) []) pcod) = MEither.do
-      return $ SigmaTy x dom !(applyReduce sig omega cod pcod)
-    applyReduceNu sig omega (SigmaTy x dom cod) p = error (range p)
-    applyReduceNu sig omega UniverseTy p = error (range p)
-    applyReduceNu sig omega NatTy p = error (range p)
-    applyReduceNu sig omega ZeroTy p = error (range p)
-    applyReduceNu sig omega OneTy p = error (range p)
-    applyReduceNu sig omega (ContextSubstElim x y) f = assert_total $ idris_crash "applyReduceNu(_[_])"
-    applyReduceNu sig omega (SignatureSubstElim x y) f = assert_total $ idris_crash "applyReduceNu(_[_])"
-    applyReduceNu sig omega (OmegaVarElim str x) p = error (range p)
-    applyReduceNu sig omega (TyEqTy a b) (TyEqTy _ pa (App _ (Underscore _) [])) = MEither.do
-      return (TyEqTy !(applyReduce sig omega a pa) b)
-    applyReduceNu sig omega (TyEqTy a b) (TyEqTy _ (App _ (Underscore _) []) pb) = MEither.do
-      return (TyEqTy a !(applyReduce sig omega b pb))
-    applyReduceNu sig omega (TyEqTy a b) p = error (range p)
-    applyReduceNu sig omega (ElEqTy a b ty) (ElEqTy _ pa (App _ (Underscore _) []) (App _ (Underscore _) [])) = MEither.do
-      return (ElEqTy !(applyReduce sig omega a pa) b ty)
-    applyReduceNu sig omega (ElEqTy a b ty) (ElEqTy _ (App _ (Underscore _) []) pb (App _ (Underscore _) [])) = MEither.do
-      return (ElEqTy a !(applyReduce sig omega b pb) ty)
-    applyReduceNu sig omega (ElEqTy a b ty) (ElEqTy _ (App _ (Underscore _) []) (App _ (Underscore _) []) pty) = MEither.do
-      return (ElEqTy a b !(applyReduce sig omega ty pty))
-    applyReduceNu sig omega (ElEqTy a b ty) p = error (range p)
-
-    public export
-    applyReduce : Signature -> Omega -> Typ -> OpFreeTerm -> M (Either Range Typ)
-    applyReduce sig omega t p = MEither.do
-      applyReduceNu sig omega !(liftM $ openEval sig omega t) p
-
-  namespace Elem
-    ||| Try applying reduce tactic on a well-typed term
-    ||| Γ ⊦ t : T
-    ||| or
-    ||| Γ ⊦ T type
-    ||| The term must be head-neutral w.r.t. open evaluation
-    ||| OpFreeTerm must represent a valid path!
-    ||| See Surface/Language for a description of being a valid path.
-    public export
-    applyReduceNu : Signature -> Omega -> Elem -> OpFreeTerm -> M (Either Range Elem)
-    applyReduceNu sig omega el (App _ (Tm _ tm) []) = MEither.do
-      applyReduce sig omega el tm
-    applyReduceNu sig omega (PiTy x dom cod) (PiTy r _ pdom (App _ (Underscore _) [])) = MEither.do
-      return $ PiTy x !(applyReduce sig omega dom pdom) cod
-    applyReduceNu sig omega (PiTy x dom cod) (FunTy r pdom (App _ (Underscore _) [])) = MEither.do
-      return $ PiTy x !(applyReduce sig omega dom pdom) cod
-    applyReduceNu sig omega (PiTy x dom cod) (PiTy r _ (App _ (Underscore _) []) pcod) = MEither.do
-      return $ PiTy x dom !(applyReduce sig omega cod pcod)
-    applyReduceNu sig omega (PiTy x dom cod) (FunTy r (App _ (Underscore _) []) pcod) = MEither.do
-      return $ PiTy x dom !(applyReduce sig omega cod pcod)
-    applyReduceNu sig omega (PiTy x dom cod) p = error (range p)
-    applyReduceNu sig omega (ImplicitPiTy x dom cod) (ImplicitPiTy r _ pdom (App _ (Underscore _) [])) = MEither.do
-      return $ ImplicitPiTy x !(applyReduce sig omega dom pdom) cod
-    applyReduceNu sig omega (ImplicitPiTy x dom cod) (ImplicitPiTy r _ (App _ (Underscore _) []) pcod) = MEither.do
-      return $ ImplicitPiTy x dom !(applyReduce sig omega cod pcod)
-    applyReduceNu sig omega (ImplicitPiTy x dom cod) p = error (range p)
-    applyReduceNu sig omega (SigmaTy x dom cod) (SigmaTy r _ pdom (App _ (Underscore _) [])) = MEither.do
-      return $ SigmaTy x !(applyReduce sig omega dom pdom) cod
-    applyReduceNu sig omega (SigmaTy x dom cod) (SigmaTy r _ (App _ (Underscore _) []) pcod) = MEither.do
-      return $ SigmaTy x dom !(applyReduce sig omega cod pcod)
-    applyReduceNu sig omega (SigmaTy x dom cod) p = error (range p)
-    applyReduceNu sig omega (PiVal x a b body) (PiVal r _ pbody) = MEither.do
-      return $ PiVal x a b !(applyReduce sig omega body pbody)
-    applyReduceNu sig omega (PiVal x a b body) p = error (range p)
-    applyReduceNu sig omega (ImplicitPiVal x a b body) (ImplicitPiVal r _ pbody) = MEither.do
-      return $ ImplicitPiVal x a b !(applyReduce sig omega body pbody)
-    applyReduceNu sig omega (ImplicitPiVal x a b body) p = error (range p)
-    applyReduceNu sig omega (SigmaVal a b) (SigmaVal r pa (App _ (Underscore _) [])) = MEither.do
-      return $ SigmaVal !(applyReduce sig omega a pa) b
-    applyReduceNu sig omega (SigmaVal a b) (SigmaVal r (App _ (Underscore _) []) pb) = MEither.do
-      return $ SigmaVal a !(applyReduce sig omega b pb)
-    applyReduceNu sig omega (SigmaVal a b) p = error (range p)
-    -- ⟦(x ↦ f) e | ☐⟧ = f[e/x]
-    applyReduceNu sig omega (PiElim f x a b e) (App r (Box _) []) = MEither.do
-      case !(liftM $ openEval sig omega f) of
-        PiVal _ _ _ body => MEither.do
-          return (ContextSubstElim body (Ext Id e))
-        _ => error r
-    applyReduceNu sig omega (PiElim f x a b e) (App r h es) = MEither.do
-      let es' = cast {to = SnocList (Range, OpFreeElimEntry)} es
-      case es' of
-        [<] => error r
-        (es :< (_, Arg ([], App _ (Underscore _) []))) => MEither.do
-          return $ PiElim !(applyReduce sig omega f (App r h (cast es))) x a b e
-        (es :< (_, Arg ([], pe))) => MEither.do
-          return $ PiElim f x a b !(applyReduce sig omega e pe)
-        (es :< (r, _)) => MEither.do
-          error r
-    applyReduceNu sig omega (PiElim f x a b e) p = error (range p)
-    -- ⟦({x} ↦ f) e | ☐⟧ = f[e/x]
-    applyReduceNu sig omega (ImplicitPiElim f x a b e) (App r (Box _) []) = MEither.do
-      case !(liftM $ openEval sig omega f) of
-        ImplicitPiVal _ _ _ body => MEither.do
-          return (ContextSubstElim body (Ext Id e))
-        _ => error r
-    applyReduceNu sig omega (ImplicitPiElim f x a b e) (App r h es) = MEither.do
-      let es' = cast {to = SnocList (Range, OpFreeElimEntry)} es
-      case es' of
-        [<] => error r
-        (es :< (_, Arg ([], App _ (Underscore _) []))) => MEither.do
-          return $ ImplicitPiElim !(applyReduce sig omega f (App r h (cast es))) x a b e
-        (es :< (_, Arg ([], pe))) => MEither.do
-          return $ ImplicitPiElim f x a b !(applyReduce sig omega e pe)
-        (es :< (r, _)) => MEither.do
-          error r
-    applyReduceNu sig omega (ImplicitPiElim f x a b e) p = error (range p)
-    -- ⟦(a, b) .π₁ | ☐⟧ = a
-    applyReduceNu sig omega (SigmaElim1 f x a b) (App r (Box _) []) = MEither.do
-      case !(liftM $ openEval sig omega f) of
-        SigmaVal p q => MEither.do
-          return p
-        _ => error r
-    applyReduceNu sig omega (SigmaElim1 f x a b) (App r h es) = MEither.do
-      let es' = cast {to = SnocList (Range, OpFreeElimEntry)} es
-      case es' of
-        [<] => error r
-        (es :< (_, Arg ([], App _ (Underscore _) []))) => MEither.do
-          return $ SigmaElim1 !(applyReduce sig omega f (App r h (cast es))) x a b
-        (es :< (_, Pi1)) => MEither.do
-          return $ SigmaElim1 !(applyReduce sig omega f (App r h (cast es))) x a b
-        (es :< (r, _)) => MEither.do
-          error r
-    applyReduceNu sig omega (SigmaElim1 f x a b) p = error (range p)
-    -- ⟦(a, b) .π₂ | ☐⟧ = b
-    applyReduceNu sig omega (SigmaElim2 f x a b) (App r (Box _) []) = MEither.do
-      case !(liftM $ openEval sig omega f) of
-        SigmaVal p q => MEither.do
-          return q
-        _ => error r
-    applyReduceNu sig omega (SigmaElim2 f x a b) (App r h es) = MEither.do
-      let es' = cast {to = SnocList (Range, OpFreeElimEntry)} es
-      case es' of
-        [<] => error r
-        (es :< (_, Arg ([], App _ (Underscore _) []))) => MEither.do
-          return $ SigmaElim2 !(applyReduce sig omega f (App r h (cast es))) x a b
-        (es :< (_, Pi2)) => MEither.do
-          return $ SigmaElim2 !(applyReduce sig omega f (App r h (cast es))) x a b
-        (es :< (r, _)) => MEither.do
-          error r
-    applyReduceNu sig omega (SigmaElim2 f x a b) p = error (range p)
-    applyReduceNu sig omega NatVal0 p = error (range p)
-    applyReduceNu sig omega (NatVal1 t) (App r (NatVal1 _) [(_, Arg ([], p))]) = MEither.do
-      return $ NatVal1 !(applyReduce sig omega t p)
-    applyReduceNu sig omega (NatVal1 t) p = error (range p)
-    applyReduceNu sig omega OneVal p = error (range p)
-    applyReduceNu sig omega NatTy p = error (range p)
-    applyReduceNu sig omega ZeroTy p = error (range p)
-    applyReduceNu sig omega OneTy p = error (range p)
-    applyReduceNu sig omega (ZeroElim t) p = error (range p)
-    -- ⟦ℕ-elim (x. A) z (x. h. s) 0 | ☐⟧ = z
-    -- ⟦ℕ-elim (x. A) z (x. h. s) (S t) | ☐⟧ = s(t/x, ℕ-elim (x. A) z (x. h. s) t/h)
-    applyReduceNu sig omega (NatElim x schema z y h s t) (App r (Box _) []) = MEither.do
-      case !(liftM $ openEval sig omega t) of
-        NatVal0 => return z
-        NatVal1 t => return (ContextSubstElim s (Ext (Ext Id t) (NatElim x schema z y h s t)))
-        _ => error r
-    applyReduceNu sig omega (NatElim x schema z y h s t) (App r (NatElim _)
-                                                              [(_, Arg ([], pschema)),
-                                                               (_, Arg ([], pz)),
-                                                               (_, Arg ([], ps)),
-                                                               (_, Arg ([], pt))]
-                                                         ) = MEither.do
-      case (pschema, pz, ps, pt) of
-        (pschema, App _ (Underscore _) [], App _ (Underscore _) [], App _ (Underscore _) []) => MEither.do
-          return (NatElim x !(applyReduce sig omega schema pschema) z y h s t)
-        (App _ (Underscore _) [], pz, App _ (Underscore _) [], App _ (Underscore _) []) => MEither.do
-          return (NatElim x schema !(applyReduce sig omega z pz) y h s t)
-        (App _ (Underscore _) [], App _ (Underscore _) [], ps, App _ (Underscore _) []) => MEither.do
-          return (NatElim x schema z y h !(applyReduce sig omega s ps) t)
-        (App _ (Underscore _) [], App _ (Underscore _) [], App _ (Underscore _) [], pt) => MEither.do
-          return (NatElim x schema z y h s !(applyReduce sig omega t pt))
-        _ => error r
-    applyReduceNu sig omega (NatElim x schema z y h s t) p = error (range p)
-    applyReduceNu sig omega (ContextSubstElim x y) f = assert_total $ idris_crash "applyReduceNu(_[_])"
-    applyReduceNu sig omega (SignatureSubstElim x y) f = assert_total $ idris_crash "applyReduceNu(_[_])"
-    applyReduceNu sig omega (ContextVarElim k) p = error (range p)
-    -- ⟦(Γ ⊦ χ ≔ t : A) σ | ☐⟧ = t(σ)
-    applyReduceNu sig omega (SignatureVarElim x sigma) p = MEither.do
-      case lookupSignature sig x of
-        Just (x, LetElemEntry ctx rhs ty) =>
-          return (ContextSubstElim rhs sigma)
-        Just (x, _) => error (range p)
-        Nothing => throw "applyReduceNu(SignatureVarElim)"
-    applyReduceNu sig omega (OmegaVarElim str x) p = error (range p)
-    applyReduceNu sig omega (TyEqTy a b) (TyEqTy _ pa (App _ (Underscore _) [])) = MEither.do
-      return (TyEqTy !(applyReduce sig omega a pa) b)
-    applyReduceNu sig omega (TyEqTy a b) (TyEqTy _ (App _ (Underscore _) []) pb) = MEither.do
-      return (TyEqTy a !(applyReduce sig omega b pb))
-    applyReduceNu sig omega (TyEqTy a b) p = error (range p)
-    applyReduceNu sig omega (ElEqTy a b ty) (ElEqTy _ pa (App _ (Underscore _) []) (App _ (Underscore _) [])) = MEither.do
-      return (ElEqTy !(applyReduce sig omega a pa) b ty)
-    applyReduceNu sig omega (ElEqTy a b ty) (ElEqTy _ (App _ (Underscore _) []) pb (App _ (Underscore _) [])) = MEither.do
-      return (ElEqTy a !(applyReduce sig omega b pb) ty)
-    applyReduceNu sig omega (ElEqTy a b ty) (ElEqTy _ (App _ (Underscore _) []) (App _ (Underscore _) []) pty) = MEither.do
-      return (ElEqTy a b !(applyReduce sig omega ty pty))
-    applyReduceNu sig omega (ElEqTy a b ty) p = error (range p)
-    applyReduceNu sig omega TyEqVal p = error (range p)
-    applyReduceNu sig omega ElEqVal p = error (range p)
-
-    public export
-    applyReduce : Signature -> Omega -> Elem -> OpFreeTerm -> M (Either Range Elem)
-    applyReduce sig omega t p = MEither.do
-      applyReduceNu sig omega !(liftM $ openEval sig omega t) p
diff --git a/src/idris/Nova/Surface/Tactic/Unfold.idr b/src/idris/Nova/Surface/Tactic/Unfold.idr
new file mode 100644
index 0000000..2c872ae
--- /dev/null
+++ b/src/idris/Nova/Surface/Tactic/Unfold.idr
@@ -0,0 +1,243 @@
+module Nova.Surface.Tactic.Unfold
+
+import Data.Fin
+import Data.Location
+import Data.SnocList
+import Data.Util
+
+import Nova.Core.Context
+import Nova.Core.Language
+import Nova.Core.Monad
+import Nova.Core.Evaluation
+import Nova.Core.Conversion
+
+import Nova.Surface.Language
+
+-- This module contains support code for the unfold tactic
+-- This tactic unfolds the head symbol once and computes normal form of the result
+
+mutual
+  namespace Typ
+    ||| Try applying reduce tactic on a well-typed term
+    ||| Γ ⊦ t : T
+    ||| or
+    ||| Γ ⊦ T type
+    ||| The term must be head-neutral w.r.t. open evaluation
+    ||| OpFreeTerm must represent a valid path!
+    ||| See Surface/Language for a description of being a valid path.
+    public export
+    applyUnfoldNu : Signature -> Omega -> SnocList VarName -> Typ -> OpFreeTerm -> M (Either Range Typ)
+    applyUnfoldNu sig omega ctx el (App _ (Tm _ tm) []) = MEither.do
+      applyUnfold sig omega ctx el tm
+    applyUnfoldNu sig omega ctx el (App _ (Underscore _) []) = MEither.do
+      return el
+    applyUnfoldNu sig omega ctx (El el) path = MEither.do
+      return $ El !(applyUnfold sig omega ctx el path)
+    applyUnfoldNu sig omega ctx (PiTy x dom cod) (PiTy r _ pdom pcod) = MEither.do
+      return $ PiTy x !(applyUnfold sig omega ctx dom pdom) !(applyUnfold sig omega (ctx :< x) cod pcod)
+    applyUnfoldNu sig omega ctx (PiTy x dom cod) (FunTy r pdom pcod) = MEither.do
+      return $ PiTy x !(applyUnfold sig omega ctx dom pdom) !(applyUnfold sig omega (ctx :< x) cod pcod)
+    applyUnfoldNu sig omega ctx (PiTy x dom cod) p = error (range p)
+    applyUnfoldNu sig omega ctx (ImplicitPiTy x dom cod) (ImplicitPiTy r _ pdom pcod) = MEither.do
+      return $ ImplicitPiTy x !(applyUnfold sig omega ctx dom pdom) !(applyUnfold sig omega (ctx :< x) cod pcod)
+    applyUnfoldNu sig omega ctx (ImplicitPiTy x dom cod) p = error (range p)
+    applyUnfoldNu sig omega ctx (SigmaTy x dom cod) (SigmaTy r _ pdom pcod) = MEither.do
+      return $ SigmaTy x !(applyUnfold sig omega ctx dom pdom) !(applyUnfold sig omega (ctx :< x) cod pcod)
+    applyUnfoldNu sig omega ctx (SigmaTy x dom cod) p = error (range p)
+    applyUnfoldNu sig omega ctx UniverseTy p = error (range p)
+    applyUnfoldNu sig omega ctx NatTy p = error (range p)
+    applyUnfoldNu sig omega ctx ZeroTy p = error (range p)
+    applyUnfoldNu sig omega ctx OneTy p = error (range p)
+    applyUnfoldNu sig omega ctx (ContextSubstElim x y) f = assert_total $ idris_crash "applyUnfoldNu(_[_])"
+    applyUnfoldNu sig omega ctx (SignatureSubstElim x y) f = assert_total $ idris_crash "applyUnfoldNu(_[_])"
+    applyUnfoldNu sig omega ctx (OmegaVarElim str x) p = error (range p)
+    applyUnfoldNu sig omega ctx (TyEqTy a b) (TyEqTy _ pa pb) = MEither.do
+      return (TyEqTy !(applyUnfold sig omega ctx a pa) !(applyUnfold sig omega ctx b pb))
+    applyUnfoldNu sig omega ctx (TyEqTy a b) p = error (range p)
+    applyUnfoldNu sig omega ctx (ElEqTy a b ty) (ElEqTy _ pa pb pty) = MEither.do
+      return (ElEqTy !(applyUnfold sig omega ctx a pa) !(applyUnfold sig omega ctx b pb) !(applyUnfold sig omega ctx ty pty))
+    applyUnfoldNu sig omega ctx (ElEqTy a b ty) p = error (range p)
+
+    public export
+    applyUnfold : Signature -> Omega -> SnocList VarName -> Typ -> OpFreeTerm -> M (Either Range Typ)
+    applyUnfold sig omega ctx t p = MEither.do
+      applyUnfoldNu sig omega ctx !(liftM $ openEval sig omega t) p
+
+  namespace Elem
+    ||| Try applying reduce tactic on a well-typed term
+    ||| Γ ⊦ t : T
+    ||| or
+    ||| Γ ⊦ T type
+    ||| The term must be head-neutral w.r.t. open evaluation
+    ||| OpFreeTerm must represent a valid path!
+    ||| See Surface/Language for a description of being a valid path.
+    public export
+    applyUnfoldNu : Signature -> Omega -> SnocList VarName -> Elem -> OpFreeTerm -> M (Either Range Elem)
+    applyUnfoldNu sig omega ctx el (App _ (Tm _ tm) []) = MEither.do
+      applyUnfold sig omega ctx el tm
+    applyUnfoldNu sig omega ctx here (App r (Box _) []) = MEither.do
+      here <- applyUnfoldNuHelper sig omega here r
+      liftM $ openEval sig omega here
+    applyUnfoldNu sig omega ctx here (App r (Underscore _) []) = MEither.do
+      return here
+    applyUnfoldNu sig omega ctx (PiTy x dom cod) (PiTy r _ pdom pcod) = MEither.do
+      return $ PiTy x !(applyUnfold sig omega ctx dom pdom) !(applyUnfold sig omega (ctx :< x) cod pcod)
+    applyUnfoldNu sig omega ctx (PiTy x dom cod) (FunTy r pdom pcod) = MEither.do
+      return $ PiTy x !(applyUnfold sig omega ctx dom pdom) !(applyUnfold sig omega (ctx :< x) cod pcod)
+    applyUnfoldNu sig omega ctx (PiTy x dom cod) p = error (range p)
+    applyUnfoldNu sig omega ctx (ImplicitPiTy x dom cod) (ImplicitPiTy r _ pdom pcod) = MEither.do
+      return $ ImplicitPiTy x !(applyUnfold sig omega ctx dom pdom) !(applyUnfold sig omega (ctx :< x) cod pcod)
+    applyUnfoldNu sig omega ctx (ImplicitPiTy x dom cod) p = error (range p)
+    applyUnfoldNu sig omega ctx (SigmaTy x dom cod) (SigmaTy r _ pdom pcod) = MEither.do
+      return $ SigmaTy x !(applyUnfold sig omega ctx dom pdom) !(applyUnfold sig omega (ctx :< x) cod pcod)
+    applyUnfoldNu sig omega ctx (SigmaTy x dom cod) (ProdTy r pdom pcod) = MEither.do
+      return $ SigmaTy x !(applyUnfold sig omega ctx dom pdom) !(applyUnfold sig omega (ctx :< x) cod pcod)
+    applyUnfoldNu sig omega ctx (SigmaTy x dom cod) p = error (range p)
+    applyUnfoldNu sig omega ctx (PiVal x a b body) (PiVal r _ pbody) = MEither.do
+      return $ PiVal x a b !(applyUnfold sig omega (ctx :< x) body pbody)
+    applyUnfoldNu sig omega ctx (PiVal x a b body) p = error (range p)
+    applyUnfoldNu sig omega ctx (ImplicitPiVal x a b body) (ImplicitPiVal r _ pbody) = MEither.do
+      return $ ImplicitPiVal x a b !(applyUnfold sig omega (ctx :< x) body pbody)
+    applyUnfoldNu sig omega ctx (ImplicitPiVal x a b body) p = error (range p)
+    applyUnfoldNu sig omega ctx (SigmaVal a b) (SigmaVal r pa pb) = MEither.do
+      return $ SigmaVal !(applyUnfold sig omega ctx a pa) !(applyUnfold sig omega ctx b pb)
+    applyUnfoldNu sig omega ctx (SigmaVal a b) p = error (range p)
+    applyUnfoldNu sig omega ctx (PiElim f x a b e) (App r h es) = MEither.do
+      let es' = cast {to = SnocList (Range, OpFreeElimEntry)} es
+      case es' of
+        [<] => error r
+        (es :< (_, Arg ([], pe))) => MEither.do
+          return $ PiElim !(applyUnfold sig omega ctx f (App r h (cast es))) x a b !(applyUnfold sig omega ctx e pe)
+        (es :< (r, _)) => MEither.do
+          error r
+    applyUnfoldNu sig omega ctx (PiElim f x a b e) p = error (range p)
+    applyUnfoldNu sig omega ctx (ImplicitPiElim f x a b e) (App r h es) = MEither.do
+      let es' = cast {to = SnocList (Range, OpFreeElimEntry)} es
+      case es' of
+        (es :< (_, ImplicitArg pe)) => MEither.do
+          return $ ImplicitPiElim !(applyUnfold sig omega ctx f (App r h (cast es))) x a b !(applyUnfold sig omega ctx e pe)
+        es => MEither.do
+          return $ ImplicitPiElim !(applyUnfold sig omega ctx f (App r h (cast es))) x a b e
+    applyUnfoldNu sig omega ctx (ImplicitPiElim f x a b e) p = MEither.do
+      return $ ImplicitPiElim !(applyUnfold sig omega ctx f p) x a b e
+    applyUnfoldNu sig omega ctx (SigmaElim1 f x a b) (App r h es) = MEither.do
+      let es' = cast {to = SnocList (Range, OpFreeElimEntry)} es
+      case es' of
+        [<] => error r
+        (es :< (_, Pi1)) => MEither.do
+          return $ SigmaElim1 !(applyUnfold sig omega ctx f (App r h (cast es))) x a b
+        (es :< (r, _)) => MEither.do
+          error r
+    applyUnfoldNu sig omega ctx (SigmaElim1 f x a b) p = error (range p)
+    applyUnfoldNu sig omega ctx (SigmaElim2 f x a b) (App r h es) = MEither.do
+      let es' = cast {to = SnocList (Range, OpFreeElimEntry)} es
+      case es' of
+        [<] => error r
+        (es :< (_, Pi2)) => MEither.do
+          return $ SigmaElim2 !(applyUnfold sig omega ctx f (App r h (cast es))) x a b
+        (es :< (r, _)) => MEither.do
+          error r
+    applyUnfoldNu sig omega ctx (SigmaElim2 f x a b) p = error (range p)
+    applyUnfoldNu sig omega ctx NatVal0 p = error (range p)
+    applyUnfoldNu sig omega ctx (NatVal1 t) (App r (NatVal1 _) [(_, Arg ([], p))]) = MEither.do
+      return $ NatVal1 !(applyUnfold sig omega ctx t p)
+    applyUnfoldNu sig omega ctx (NatVal1 t) p = error (range p)
+    applyUnfoldNu sig omega ctx OneVal p = error (range p)
+    applyUnfoldNu sig omega ctx NatTy p = error (range p)
+    applyUnfoldNu sig omega ctx ZeroTy p = error (range p)
+    applyUnfoldNu sig omega ctx OneTy p = error (range p)
+    applyUnfoldNu sig omega ctx (ZeroElim t) p = error (range p)
+    applyUnfoldNu sig omega ctx (NatElim x schema z y h s t) (App r (NatElim _)
+                                                              [(_, Arg ([], pschema)),
+                                                               (_, Arg ([], pz)),
+                                                               (_, Arg ([], ps)),
+                                                               (_, Arg ([], pt))]
+                                                         ) = MEither.do
+      return (NatElim x !(applyUnfold sig omega (ctx :< x) schema pschema)
+                        !(applyUnfold sig omega ctx z pz)
+                        y
+                        h
+                        !(applyUnfold sig omega (ctx :< y :< h) s ps)
+                        !(applyUnfold sig omega ctx t pt)
+             )
+    applyUnfoldNu sig omega ctx (NatElim x schema z y h s t) p = error (range p)
+    applyUnfoldNu sig omega ctx (ContextSubstElim x y) f = assert_total $ idris_crash "applyUnfoldNu(_[_])"
+    applyUnfoldNu sig omega ctx (SignatureSubstElim x y) f = assert_total $ idris_crash "applyUnfoldNu(_[_])"
+    applyUnfoldNu sig omega ctx (ContextVarElim k) (App r (Var _ y) []) = MEither.do
+      case mbIndex k ctx of
+        Just (_, x, _) =>
+          case x == y of
+            True => return (ContextVarElim k)
+            False => error r
+        Nothing => error r
+    applyUnfoldNu sig omega ctx (ContextVarElim k) p = error (range p)
+    applyUnfoldNu sig omega ctx (OmegaVarElim str x) p = error (range p)
+    applyUnfoldNu sig omega ctx (TyEqTy a b) (TyEqTy _ pa pb) = MEither.do
+      return (TyEqTy !(applyUnfold sig omega ctx a pa) !(applyUnfold sig omega ctx b pb))
+    applyUnfoldNu sig omega ctx (TyEqTy a b) p = error (range p)
+    applyUnfoldNu sig omega ctx (ElEqTy a b ty) (ElEqTy _ pa pb pty) = MEither.do
+      return (ElEqTy !(applyUnfold sig omega ctx a pa) !(applyUnfold sig omega ctx b pb) !(applyUnfold sig omega ctx ty pty))
+    applyUnfoldNu sig omega ctx (ElEqTy a b ty) p = error (range p)
+    applyUnfoldNu sig omega ctx TyEqVal p = error (range p)
+    applyUnfoldNu sig omega ctx ElEqVal p = error (range p)
+    applyUnfoldNu sig omega ctx tm@(SignatureVarElim x subst) (App r (Var _ y) []) = MEither.do
+      case !(liftM $ conv sig omega subst Terminal) of
+        True =>
+          case lookupSignature sig x of
+            Just (x, _) =>
+              case x == y of
+                True => return tm
+                False => error r
+            Nothing => throw "applyUnfoldNu(SignatureVarElim)"
+        False => error r
+    applyUnfoldNu sig omega ctx (SignatureVarElim x sigma) p = throw "applyUnfold(1): \{show p}"
+
+    public export
+    applyUnfoldNuHelper : Signature -> Omega -> Elem -> Range -> M (Either Range Elem)
+    applyUnfoldNuHelper sig omega (PiTy str x y) r = error r
+    applyUnfoldNuHelper sig omega (ImplicitPiTy str x y) r = error r
+    applyUnfoldNuHelper sig omega (SigmaTy str x y) r = error r
+    applyUnfoldNuHelper sig omega (PiVal str x y z) r = error r
+    applyUnfoldNuHelper sig omega (ImplicitPiVal str x y z) r = error r
+    applyUnfoldNuHelper sig omega (SigmaVal x y) r = error r
+    applyUnfoldNuHelper sig omega (PiElim f x dom cod e) r = MEither.do
+      f <- applyUnfoldNuHelper sig omega f r
+      return (PiElim f x dom cod e)
+    applyUnfoldNuHelper sig omega (ImplicitPiElim f x dom cod e) r = MEither.do
+      f <- applyUnfoldNuHelper sig omega f r
+      return (ImplicitPiElim f x dom cod e)
+    applyUnfoldNuHelper sig omega (SigmaElim1 f x dom cod) r = MEither.do
+      f <- applyUnfoldNuHelper sig omega f r
+      return (SigmaElim1 f x dom cod)
+    applyUnfoldNuHelper sig omega (SigmaElim2 f x dom cod) r = MEither.do
+      f <- applyUnfoldNuHelper sig omega f r
+      return (SigmaElim2 f x dom cod)
+    applyUnfoldNuHelper sig omega NatVal0 r = error r
+    applyUnfoldNuHelper sig omega (NatVal1 x) r = error r
+    applyUnfoldNuHelper sig omega NatTy r = error r
+    applyUnfoldNuHelper sig omega (NatElim x schema z y h s t) r = MEither.do
+      t <- applyUnfoldNuHelper sig omega t r
+      return (NatElim x schema z y h s t)
+    applyUnfoldNuHelper sig omega (ContextSubstElim x y) r = assert_total $ idris_crash "applyUnfoldNuHelper(ContextSubstElim)"
+    applyUnfoldNuHelper sig omega (SignatureSubstElim x y) r = assert_total $ idris_crash "applyUnfoldNuHelper(SignatureSubstElim)"
+    applyUnfoldNuHelper sig omega (ContextVarElim k) r = error r
+    applyUnfoldNuHelper sig omega (SignatureVarElim x sigma) r = M.do
+      case lookupSignature sig x of
+        Just (x, LetElemEntry ctx rhs ty) =>
+          return (ContextSubstElim rhs sigma)
+        Just (x, _) => error r
+        Nothing => throw "applyUnfoldNu(SignatureVarElim)"
+    applyUnfoldNuHelper sig omega (OmegaVarElim str x) r = error r
+    applyUnfoldNuHelper sig omega (TyEqTy x y) r = error r
+    applyUnfoldNuHelper sig omega (ElEqTy x y z) r = error r
+    applyUnfoldNuHelper sig omega TyEqVal r = error r
+    applyUnfoldNuHelper sig omega ElEqVal r = error r
+    applyUnfoldNuHelper sig omega ZeroTy r = error r
+    applyUnfoldNuHelper sig omega OneTy r = error r
+    applyUnfoldNuHelper sig omega OneVal r = error r
+    applyUnfoldNuHelper sig omega (ZeroElim x) r = error r
+
+    public export
+    applyUnfold : Signature -> Omega -> SnocList VarName -> Elem -> OpFreeTerm -> M (Either Range Elem)
+    applyUnfold sig omega ctx t p = MEither.do
+      applyUnfoldNu sig omega ctx !(liftM $ openEval sig omega t) p
diff --git a/src/nova/Test.nova b/src/nova/Test.nova
index 5dbdd0a..93157e7 100644
--- a/src/nova/Test.nova
+++ b/src/nova/Test.nova
@@ -37,7 +37,7 @@ let pred' : ℕ → ℕ
 
 define pred'-S : (x : ℕ) → pred' (S x) ≡ x ∈ ℕ
                ≔ x ↦ tac
-                   reduce ☐ _ _ ≡ _ ∈ _;
+                   unfold ☐ ≡ _ ∈ _;
                    trivial;
 
 define S-cong-inv-H0 : {x y : ℕ} → (e : pred' (S x) ≡ pred' (S y) ∈ ?) → x ≡ y ∈ ?
@@ -53,18 +53,18 @@ let Vect : ℕ → 𝕌 → 𝕌
          ≔ n A ↦ ℕ-elim (x. 𝕌) 𝟙 (x.H. A ⨯ H) n
 
 let nil : {A : 𝕌} → Vect Z A
-        ≔ {A} ↦ tac reduce ☐ _ _;
+        ≔ {A} ↦ tac unfold ☐;
                     exact tt;
 
 let Vect-Z : {A : 𝕌} → Vect Z A ≡ 𝟙 ∈ 𝕌
                ≔ {A} ↦ tac
-                     reduce ☐ _ _ ≡ _ ∈ _;
+                     unfold ☐ ≡ _ ∈ _;
                      trivial;
 
 let Vect-S : {A : 𝕌} → {n : ℕ} → Vect (S n) A ≡ A ⨯ Vect n A ∈ 𝕌
                ≔ {A n} ↦ tac
-                     reduce ☐ _ _ ≡ _ ∈ _;
-                     reduce _ ≡ ((x : _) ⨯ ☐ _ _) ∈ _;
+                     unfold ☐ ≡ _ ∈ _;
+                     unfold _ ≡ ((x : _) ⨯ ☐ _ _) ∈ _;
                      trivial;
 
 define nil-unique : {A : 𝕌} → (xs : Vect Z A) → xs ≡ nil {A} ∈ Vect Z A
@@ -91,7 +91,7 @@ define Vect-elim-H : {A : 𝕌}
                    → P (S n) (xs .π₁ :: xs .π₂)
                    → P (S n) (tac rewrite⁻¹ ☐ Vect-S; exact (xs .π₁ , xs .π₂);)
                    ≔ {A} ↦ P n xs ↦ tac
-                       reduce _ (☐ _ _ _ _) → _;
+                       unfold P _ ☐ → _;
                        exact id;
 
 let Vect-elim : {A : 𝕌}
@@ -123,7 +123,7 @@ define Vect-elim-nil : {A : 𝕌}
                      → (onCons : (n : ℕ) → (x : A) → (xs : Vect n A) → P n xs → P (S n) (x :: xs))
                      → Vect-elim P onNil onCons nil ≡ onNil ∈ ?
                      ≔ {A} ↦ P onNil onCons ↦ tac
-                          reduce ☐ _ _ _ _ _ _ ≡ _ ∈ _;
+                          unfold ☐ ≡ _ ∈ _;
                           trivial;
 
 define Vect-elim-cons : {A : 𝕌}
@@ -135,14 +135,14 @@ define Vect-elim-cons : {A : 𝕌}
                       → (xs : Vect n A)
                       → Vect-elim P onNil onCons (x :: xs) ≡ onCons n x xs (Vect-elim P onNil onCons xs) ∈ ?
                       ≔ {A n} ↦ P onNil onCons x xs ↦ tac
-                          reduce ☐ _ _ _ _ _ _ ≡ _ ∈ _;
-                          reduce ☐ _ _ ≡ _ ∈ _;
-                          reduce _ _ (☐ _ _ _ _ .π₁) _ _ ≡ _ ∈ _;
-                          reduce _ _ _ (☐ _ _ _ _ .π₂) _ ≡ _ ∈ _;
-                          reduce _ _ _ _ (ℕ-elim _ _ (xs ↦ ☐ _ _ _ _) _ _) ≡ _ ∈ _;
-                          reduce _ _ _ _ (ℕ-elim _ _ _ _ (☐ _ _ _ _ .π₂)) ≡ _ ∈ _;
-                          reduce _ ≡ _ _ _ _ (☐ _ _ _ _ _ _) ∈ _;
-                          reduce _ ≡ _ _ _ _ (ℕ-elim _ _ (xs ↦ ☐ _ _ _ _) _ _) ∈ _;
+                          unfold ☐ ≡ _ ∈ _;
+                          unfold ☐ ≡ _ ∈ _;
+                          unfold onCons _ _ ☐ _ ≡ _ ∈ _;
+                          unfold onCons _ ☐ _ _ ≡ _ ∈ _;
+                          unfold onCons _ _ _ (ℕ-elim _ _ (xs ↦ ☐) n _) ≡ _ ∈ _;
+                          unfold onCons _ _ _ (ℕ-elim _ _ _ _ ☐) ≡ _ ∈ _;
+                          unfold _ ≡ onCons _ _ _ ☐ ∈ _;
+                          unfold _ ≡ onCons _ _ _ (ℕ-elim _ _ (xs ↦ ☐) n _) ∈ _;
                           trivial;
 
 
@@ -213,20 +213,20 @@ let _*_ : ℕ → ℕ → ℕ
 
 define mult-left-Z : (x : ℕ) → Z * x ≡ Z ∈ ?
                     ≔ x ↦ tac
-                        reduce ☐ _ _ ≡ _ ∈ _;
+                        unfold ☐ ≡ _ ∈ _;
                         trivial;
 
 define mult-right-Z : (x : ℕ) → x * Z ≡ Z ∈ ?
                     ≔ x ↦ tac
-                        reduce ☐ _ _ ≡ _ ∈ _;
+                        unfold ☐ ≡ _ ∈ _;
                         rewrite⁻¹ (ℕ-elim _ _ ☐ _ ≡ _ ∈ _) (plus-left-Z ?);
                         exact ℕ-elim (x. ℕ-elim (x. ℕ) Z (x.h. h) x ≡ Z ∈ ℕ) (tac trivial;) (x. h. tac exact h;) x;
 
 
 define mult-left-S : (t : ℕ) → (x : ℕ) → (S t * x) ≡ (x + t * x) ∈ ?
                    ≔ t x ↦ tac
-                       reduce ☐ _ _ ≡ _ ∈ _;
-                       reduce _ ≡ _ + ☐ _ _ ∈ _;
+                       unfold ☐ ≡ _ ∈ _;
+                       unfold _ ≡ _ + ☐ ∈ _;
                        trivial;
 
 
@@ -278,22 +278,24 @@ let _++_ : {A : 𝕌} → {m n : ℕ} → Vect m A → Vect n A → Vect (m + n)
 
 define append-left-nil : {A : 𝕌} → {n : ℕ} → (xs : Vect n A) → nil ++ xs ≡ (tac rewrite⁻¹ (_ ☐ _) (plus-left-Z ?); exact xs;) ∈ ?
                        ≔ {A n} ↦ xs ↦
-                            tac reduce ☐ _ _ _ _ _ ≡ _ ∈ _;
-                                reduce ☐ _ _ _ _ _ _ ≡ _ ∈ _;
+                            tac unfold ☐ ≡ _ ∈ _;
+                                unfold ☐ ≡ _ ∈ _;
                                 trivial;
 -- BUG:                                                                                        vvvvvvvvvvv doesn't parse as operator
 define append-left-cons : {A : 𝕌} → {m n : ℕ} → (x : A) → (xs : Vect m A) → (ys : Vect n A) → ((_::_ x xs) ++ ys ≡ (tac rewrite⁻¹ (_ ☐ _) (plus-left-S ? ?); exact x :: (xs ++ ys);) ∈ ?)
                         ≔ {A m n} ↦ x xs ys ↦ tac
-                            reduce ☐ _ _ _ _ _ ≡ _ ∈ _;
-                            reduce ☐ _ _ _ _ _ _ ≡ _ ∈ _;
-                            reduce ☐ _ _ ≡ _ ∈ _;
-                            reduce _ ≡ ☐ _ _ _ _ _ ∈ _;
-                            reduce ☐ _ _ _ _ .π₁ , _ ≡ _ ∈ _;
-                            reduce _ ≡ _ , ☐ _ _ _ _ _ ∈ _;
-                            reduce _ ≡ _ , ☐ _ _ _ _ _ _ ∈ _;
-                            reduce _ , ℕ-elim _ _ _ (☐ _ _ _ _ .π₂) ≡ _ ∈ _;
+                            unfold ☐ ≡ _ ∈ _;
+                            unfold ☐ ≡ _ ∈ _;
+                            unfold ☐ ≡ _ ∈ _;
+                            unfold _ ≡ ☐ ∈ _;
+                            unfold ☐ , _ ≡ _ ∈ _;
+                            unfold _ ≡ _ , ☐  ∈ _;
+                            unfold _ ≡ _ , ☐ ∈ _;
+                            unfold _ , ℕ-elim _ _ _ m ☐ ≡ _ ∈ _;
                             trivial;
 
+-- xs ++ [] = xs
+
 define append-right-nil : {A : 𝕌} → {n : ℕ} → (xs : Vect n A) → xs ++ nil ≡ (tac rewrite⁻¹ (_ ☐ _) (plus-right-Z ?); exact xs;) ∈ ?
                        ≔ {A n} ↦ xs ↦ Vect-elim (n xs ↦ xs ++ nil ≡ (tac rewrite⁻¹ (_ ☐ _) (plus-right-Z ?); exact xs;) ∈ ?)
                            (tac rewrite⁻¹ (☐ ≡ _ ∈ _) (append-left-nil nil); trivial;)
@@ -303,7 +305,7 @@ define append-right-nil : {A : 𝕌} → {n : ℕ} → (xs : Vect n A) → xs ++
 -- reverseH xs nil = xs
 -- reverseH xs (y :: ys) = reverseH (y :: xs) ys
 
-define reverseH : {A : 𝕌} → {m n : ℕ} → Vect m A → Vect n A → Vect (m + n) A
+let reverseH : {A : 𝕌} → {m n : ℕ} → Vect m A → Vect n A → Vect (m + n) A
                 ≔  {A m n} ↦ xs ys ↦ Vect-elim
                      (n ys ↦ (m : ℕ) → Vect m A → Vect (m + n) A)
                      (m xs ↦ tac rewrite⁻¹ (_ ☐ _) (plus-right-Z ?); exact xs;)
@@ -312,9 +314,39 @@ define reverseH : {A : 𝕌} → {m n : ℕ} → Vect m A → Vect n A → Vect
                      ys m xs
 
 
+-- reverseH xs [] = xs
+
 define reverseH-nil : {A : 𝕌} → {n : ℕ} → (xs : Vect n A) → reverseH xs nil ≡ (tac rewrite⁻¹ (_ ☐ _) (plus-right-Z ?); exact xs;) ∈ ?
-                   ≔ {A n} ↦ xs ↦ tac rewrite⁻¹ (☐ _ _ ≡ _ ∈ _) (Vect-elim-nil (n ↦ ys ↦ (m : ℕ) → Vect m A → Vect (m + n) A) ? ?); trivial;
+                   ≔ {A n} ↦ xs ↦ tac unfold ☐ ≡ _ ∈ _; rewrite⁻¹ (☐ _ _ ≡ _ ∈ _) (Vect-elim-nil (n ↦ ys ↦ (m : ℕ) → Vect m A → Vect (m + n) A) ? ?); trivial;
+
+-- reverseH xs (y :: ys) = reverse (y :: xs) ys
+
+-- reverseH xs (y :: ys) : Vect (m + S n) A
+-- reverseH (y :: xs) ys : Vect (S m + n) A
+
+define reverseH-cons : {A : 𝕌} → {m n : ℕ} → (xs : Vect m A) → (y : A) → (ys : Vect n A) →
+                         (tac rewrite (_ ☐ _) (plus-right-S ? ?); exact reverseH xs (y :: ys);)
+                            ≡
+                         (tac rewrite (_ ☐ _) (plus-left-S ? ?); exact reverseH (y :: xs) ys;)
+                            ∈
+                         Vect (S (m + n)) A
+
+-- reverseH xs (y :: ys) = reverseH (y :: xs) ys
+
+                     ≔ {A m n} ↦ xs y ys ↦ tac
+                       unfold ☐ ≡ _ ∈ _;
+                       unfold ☐ ≡ _ ∈ _;
+                       unfold ☐ ≡ _ ∈ _;
+                       unfold ℕ-elim _ _ (x ↦ ☐) _ _ _ _ ≡ _ ∈ _;
+                       unfold ℕ-elim _ _ _ _ ☐ _ _ ≡ _ ∈ _;
+                       unfold ℕ-elim _ _ _ _ _ _ (☐ :: _) ≡ _ ∈ _;
+                       unfold _ ≡ ☐ ∈ _;
+                       unfold _ ≡ ☐ ∈ _;
+                       unfold _ ≡ ℕ-elim _ _ (x ↦ ☐) _ _ _ _ ∈ _;
+                       trivial;
+
 
+-- (_::_(·) {A} {n} y ys .π₂)
 
 -- reverse : Vect m → Vect n A → Vect (m + n)
 -- reverse xs [] = xs : Vect (m + 0) A