How do I define notation that behaves like Coq’s `fix`

in that the following lines parse successfully?

```
Check myfix f n : nat := S n.
Check myfix f (n : nat) : nat := S n.
```

I cannot find a `Notation`

invocation that allows binders and correctly parses the overall type annotation. Here is a template to play around with. (I tried closed binders to see if they would play better with the `:`

part of the notation.)

```
Notation "'myfix' f x .. y : T := b" :=
(fun f => fun x => .. (fun y => b : T) ..)
(at level 0, x closed binder, y closed binder).
```