simp unfolds local def through projection

[lecopivo]

Simp unfolds local definition with zetaDelta := false if the value of local definition can be reduced with a projection.

Actual behavior:
Here is a simple example

example (x y : Nat) : let a := (x,y); a.2 = 0 := by
  intro a
  simp (config := {zetaDelta:=false})

before simp the state is:

x y: Nat
a: Nat × Nat := (x, y)
⊢ a.snd = 0

and after simp the state is:

x y: Nat
a: Nat × Nat := (x, y)
⊢ y = 0

Expected behavior:
I'm expecting for simp not to reduce a.snd to y.

Cause:
I did some digging and found out that the issue is with the calls to reduceProj? in simp which calls whnf with default settings i.e. zetaDelta := true.

Lean version: v4.9.0-rc2