feat: `eta_reduce_fun%` in cdot parser

[digama0]

This and #2267 are two implementations of the same feature, merge only one.

This modifies the desugaring for the cdot parser to apply eta-reduction to the resulting term if possible. So (· + ·) elaborates to HAdd.hAdd instead of fun x y => HAdd.hAdd x y.

This is complicated by the fact that metavariables generally capture all variables in scope, meaning that (· + ·) of unknown type elaborates to something like fun x y => @HAdd.hAdd (?m1 x y) (?m2 x y) x y, which is not an eta redex. To reliably eta reduce the expression we therefore have to wait for all the mvars to be solved, but we also can't postpone because the body of the lambda might itself be postponing, and the combination seems to make some existing test cases fail. So instead we register a secondary eta_reduce_delayed% expression which waits for the body to be resolved with no mvars, and then does the eta reduction.

[digama0]

Hm, this still isn't working, and I have another reimplementation which also isn't working. I know how to make a version which sometimes fails to eta-reduce but doesn't break anything, but I think I will need to ask for help making this work properly, I don't think I fully understand how to do this with postponement. cc: @leodemoura