FunInd: `fun_induction foo` considers let-bound FVars as atomic

In this example, the fun_induction map should not succeed: The target xs in the call to map is no really atomic, it’s just let-extracted:

def map (f : Bool → Bool) : List Bool → List Bool
  | [] => []
  | x::xs => f x::map f xs
termination_by x => x

example : let xs := List.replicate 4 true; (map f xs).length = xs.length := by
  intro xs
  fail_if_success fun_induction map

Could be fixed together with #7985 (treating all propositions as atomic).

Versions

Lean 4.20.0-nightly-2025-04-29

Impact

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

Reproduce the provided example with Lean 4.20.0-nightly-2025-04-29, then start from the fun_induction entry point and compare the behavior with issue #7985. Done means fun_induction map no longer succeeds when the target is a let-extracted local, while the reported example continues to demonstrate the corrected behavior.