A recursive abstraction (fix) followed by an lambda abstraction (fun) seems to be converted by the reader into a fix with extra arguments. For instance,

```
Set Printing All.
Check fix add x := fun y =>
match x with
| O => y
| S x' => S (add x' y)
end.
```

yields

```
fix add (x y : nat) {struct x} : nat :=
match x return nat with
| O => y
| S x' => S (add x' y)
end
: forall (_ : nat) (_ : nat), nat
```

But it’s not just the reader, it’s a conversion rule. Consider

```
Definition foo :=
fix F x := fun y => match x with
| O => y
| S x' => S y
end.
Definition foo' x y :=
match x with
| 0 => y
| S x' => S y
end.
Goal foo = foo'.
Fail reflexivity.
Abort.
Goal foo = fix F x := foo' x.
reflexivity.
Qed.
```

I’m puzzled. Did this enter the kernel with \eta-conversion? Or was it there before and I’m just ignorant of the conversion rule? Or is there some other explanation? I would be very thankful for pointers. Gert