diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index b819e39eae..ae128f47ba 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -277,13 +277,16 @@ where
   Collect forward dependencies that are not in the forbidden set, and depend on some variable in `targets`.
 
   Remark: this method assumes `targets` are free variables.
+
+  Remark: we *not* collect instance implicit arguments nor auxiliary declarations for compiling
+  recursive declarations.
 -/
 private def collectForwardDeps (targets : Array Expr) (forbidden : NameSet) : MetaM NameSet := do
   let mut s : NameSet := targets.foldl (init := {}) fun s target => s.insert target.fvarId!
   let mut r : NameSet := {}
   for localDecl in (← getLCtx) do
     unless forbidden.contains localDecl.fvarId do
-      unless localDecl.isAuxDecl do
+      unless localDecl.isAuxDecl || localDecl.binderInfo.isInstImplicit do
       if (← getMCtx).findLocalDeclDependsOn localDecl fun fvarId => s.contains fvarId then
         r := r.insert localDecl.fvarId
         s := s.insert localDecl.fvarId
diff --git a/tests/lean/run/394.lean b/tests/lean/run/394.lean
new file mode 100644
index 0000000000..1d0e284aca
--- /dev/null
+++ b/tests/lean/run/394.lean
@@ -0,0 +1,9 @@
+def casesTFOn {motive : Prop → Sort _} (P) [inst : Decidable P] : (T : motive True) → (F : motive False) → motive P :=
+  λ ht hf => match inst with
+  | isTrue H => eqTrue H ▸ ht
+  | isFalse H => eqFalse H ▸ hf
+
+example (P) [Decidable P] : ¬¬P → P := by
+  induction P using casesTFOn
+  admit
+  admit