diff --git a/src/Init/Lean/Meta/Tactic/FVarSubst.lean b/src/Init/Lean/Meta/Tactic/FVarSubst.lean
index b7d636023d..cc349eca1e 100644
--- a/src/Init/Lean/Meta/Tactic/FVarSubst.lean
+++ b/src/Init/Lean/Meta/Tactic/FVarSubst.lean
@@ -20,6 +20,8 @@ structure FVarSubst :=
 
 namespace FVarSubst
 
+def empty : FVarSubst := {}
+
 def insert (s : FVarSubst) (fvarId : FVarId) (e : Expr) : FVarSubst :=
 { map := s.map.insert fvarId e }
 
diff --git a/src/Init/Lean/Meta/Tactic/Subst.lean b/src/Init/Lean/Meta/Tactic/Subst.lean
index bd3cc3090f..3572732d44 100644
--- a/src/Init/Lean/Meta/Tactic/Subst.lean
+++ b/src/Init/Lean/Meta/Tactic/Subst.lean
@@ -57,7 +57,12 @@ withMVarContext mvarId $ do
             mvarId ← clear mvarId hFVarId;
             mvarId ← clear mvarId aFVarId;
             (newFVars, mvarId) ← introN mvarId (vars.size - 2) [] false;
-            fvarSubst ← pure {FVarSubst . }; -- TODO
+            fvarSubst ← newFVars.size.foldM
+              (fun i (fvarSubst : FVarSubst) =>
+                let var      := vars.get! i;
+                let newFVar := newFVars.get! i;
+                pure $ fvarSubst.insert var (mkFVar newFVar))
+              FVarSubst.empty;
             pure (fvarSubst, mvarId)
           };
           if depElim then do