diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index d43c4ef6ee..6c26af38ed 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -103,7 +103,7 @@ private partial def finalizeAux
           (extra,  mvarId') ← introN mvarId' nextra [] false;
           let subst := reverted.size.fold
             (fun i (subst : FVarSubst) =>
-              if i ≤ indices.size + 1 then subst
+              if i < indices.size + 1 then subst
               else
                 let revertedFVarId := reverted.get! i;
                 let newFVarId      := extra.get! (i - indices.size - 1);
@@ -173,6 +173,7 @@ withMVarContext mvarId $ do
     (majorFVarId', mvarId) ← intro1 mvarId false;
     -- Create FVarSubst with indices
     let baseSubst : FVarSubst := indices.iterate {} (fun i index subst => subst.insert index.fvarId! (indices'.get! i.val));
+    trace! `Meta.Tactic.induction ("after revert&intro" ++ Format.line ++ MessageData.ofGoal mvarId);
     -- Update indices and major
     let indices := indices'.map mkFVar;
     let majorFVarId := majorFVarId';
@@ -209,5 +210,8 @@ withMVarContext mvarId $ do
         | _ =>
          throwTacticEx `induction mvarId "major premise is not of the form (C ...)"
 
+@[init] private def regTraceClasses : IO Unit := do
+registerTraceClass `Meta.Tactic.induction
+
 end Meta
 end Lean