diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index 5c374e9e91..90a125c1f8 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -20,17 +20,14 @@ open Eqns
 structure EqnInfo extends EqnInfoCore where
   declNames       : Array Name
   declNameNonRec  : Name
-  fixedPrefixSize : Nat
   argsPacker      : ArgsPacker
   fixedParamPerms : FixedParamPerms
   deriving Inhabited
 
-
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms)
     (argsPacker : ArgsPacker) : MetaM Unit := do
-  let fixedPrefixSize := fixedParamPerms.numFixed
   preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   /-
   See issue #2327.
@@ -43,7 +40,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
       modifyEnv fun env =>
         preDefs.foldl (init := env) fun env preDef =>
           eqnInfoExt.insert env preDef.declName { preDef with
-            declNames, declNameNonRec, fixedPrefixSize, argsPacker, fixedParamPerms }
+            declNames, declNameNonRec, argsPacker, fixedParamPerms }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 473dca1fd5..f45ba69dc4 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -875,15 +875,17 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
     -- Look for _unary redexes
     if e.isAppOf eqnInfo.declNameNonRec then
       let args := e.getAppArgs
-      if eqnInfo.fixedPrefixSize + 1 ≤ args.size then
-        let packedArg := args.back!
-          let some (i, unpackedArgs) := eqnInfo.argsPacker.unpack packedArg
-            | throwError "Unexpected packedArg:{indentExpr packedArg}"
-          let e' := .const eqnInfo.declNames[i]! e.getAppFn.constLevels!
-          let e' := mkAppN e' args.pop
-          let e' := mkAppN e' unpackedArgs
-          let e' := mkAppN e' args[eqnInfo.fixedPrefixSize+1:]
-          return .continue e'
+      if h : args.size ≥ eqnInfo.fixedParamPerms.numFixed + 1 then
+        let xs := args[:eqnInfo.fixedParamPerms.numFixed]
+        let packedArg := args[eqnInfo.fixedParamPerms.numFixed]
+        let extraArgs := args[eqnInfo.fixedParamPerms.numFixed+1:]
+        let some (funIdx, ys) := eqnInfo.argsPacker.unpack packedArg
+          | throwError "Unexpected packedArg:{indentExpr packedArg}"
+        let args' := eqnInfo.fixedParamPerms.perms[funIdx]!.buildArgs xs ys
+        let e' := .const eqnInfo.declNames[funIdx]! e.getAppFn.constLevels!
+        let e' := mkAppN e' args'
+        let e' := mkAppN e' extraArgs
+        return .continue e'
 
     return .continue e)
   mkExpectedTypeHint value cleanType
@@ -902,6 +904,7 @@ def unpackMutualInduction (eqnInfo : WF.EqnInfo) : MetaM Name := do
   return inductName
 where doRealize inductName := do
   let unaryInductName ← deriveUnaryInduction eqnInfo.declNameNonRec
+  mapError (f := (m!"Cannot unpack functional cases principle {.ofConstName unaryInductName} (please report this issue)\n{indentD ·}")) do
   let ci ← getConstInfo unaryInductName
   let us := ci.levelParams
   let value := .const ci.name (us.map mkLevelParam)
@@ -930,7 +933,7 @@ where doRealize inductName := do
         return value
 
   unless ← isTypeCorrect value do
-    logError m!"failed to unpack induction principle:{indentExpr value}"
+    logError m!"final term is type incorrect:{indentExpr value}"
     check value
   let type ← inferType value
   let type ← elimOptParam type
diff --git a/tests/lean/run/issue8093.lean b/tests/lean/run/issue8093.lean
new file mode 100644
index 0000000000..fa30e5d39e
--- /dev/null
+++ b/tests/lean/run/issue8093.lean
@@ -0,0 +1,13 @@
+axiom testSorry : α
+
+def foo (n : Nat) (p : Nat) : Nat :=
+  foo (foo (n - 1) p) p
+termination_by n
+decreasing_by all_goals exact testSorry
+
+/--
+info: foo.induct (p : Nat) (motive : Nat → Prop) (case1 : ∀ (x : Nat), motive (x - 1) → motive (foo (x - 1) p) → motive x)
+  (n : Nat) : motive n
+-/
+#guard_msgs in
+#check foo.induct