"Cannot derive functional induction principle" for function involving mutual inductives

[sgraf812]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Consider the following MWE with a custom Vector (Term s) n inlined (live)

mutual
inductive Term : Unit → Type where
| con : (con : Nat) → ConArgs con s → Term s

inductive ConArgs : (n:Nat) → Unit → Type where
| nil : ConArgs 0 s
| cons : Term s → ConArgs n s → ConArgs (n+1) s
end

def ConArgs.toList : ConArgs n s → List (Term s)
| nil => []
| cons e args => e :: args.toList

private theorem ConArgs.length_toList_eq {args : ConArgs n s} : args.toList.length = n := by
  fun_induction ConArgs.toList

Steps to Reproduce

Elaborate the example

Expected behavior: I would expect the fun_induction tactic to do its thing

Actual behavior: fun_induction tactic says

Failed to realize constant ConArgs.toList.induct_unfolding:
  Cannot derive functional induction principle (please report this issue)
    type (∀ (n : Nat) (a : Unit) (t : ConArgs n a) (f : t.below), motive t t.toList) → True does not have 2 parameters

Versions

Lean 4.27.0-nightly-2025-11-30
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.