The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Thanks, Cédric, but I simplified my actual problem to make my question
easier to understand. In my original problem, unfolding FUN and
beta-reducing it does not help, because FUN does non trivial things
with the extra-parameters.

> If you need a solution, I guess this does what you want (I unfolded
> your FUN, and then β reduced it).
>
> Notation "’mylet’ f x .. y :=  t ’in’ u":=
> (let f := (fun n R => fun x => (.. (fun y => t n R) ..)) in u)
>      (x closed binder, y closed binder, at level 200, right
>      associativity).
>
> I guess addition of binders confuse Coq.