Is there a built-in tactic that would reduce `fun x => f x`

to `f`

or the other way around? `cbv`

doesn’t do that. I guess you can `rewrite eta`

, where `eta`

is the lemma below, but maybe I’m missing something even simpler.

```
Lemma eta {A B} (f : A -> B) : (fun x => f x) = f.
Proof.
cbv. (* I would like to see f = f now *)
reflexivity. (* this proof works in any case, but sometimes syntax matters (rewriting, match...) *)
Qed.
```

I thought there were situations where `fun x => f x`

is directly transformed into `f`

but I can’t seem to find an example of that.