DefEq transitivity failure for function eta

The type-checker applies function eta only when one side of the equation is a manifest lambda. But there are other forms where eta-expanding would be productive, e.g. partially applied Eq.rec. This leads to a intransitivity of defeq checking:

variable (a : true = true → Bool)

example : (@Eq.rec Bool true (fun _ _ => Bool) (a (Eq.refl true)) _) = fun h => a h := rfl
example : (fun h => a h) = a := rfl
/--
error: Type mismatch
  rfl
has type
  ?m.8 = ?m.8
but is expected to have type
  Eq.rec (a ⋯) = a
-/
#guard_msgs in
example  : (@Eq.rec Bool true (fun _ _ => Bool) (a (Eq.refl true)) _) = a := rfl

This is similar in spirit to #2258. It seems to have low practical impact, reporting it here for reference.

Start by reproducing the two rfl examples in the issue and compare the behavior with the related issue #2258. Trace the type-checker's function-eta handling for manifest lambdas and partially applied Eq.rec; done means the intended definitional-equality behavior is specified and covered by a regression test.