remove unnecessary implicit arguments in lambdas

[kim-em]

In Lean 4, when we write a lambda, the implicit arguments are introduced automatically and do not need to be named. mathport will need to remove these arguments.

See for example https://github.com/leanprover-community/mathlib3port/blob/9f61de0/Mathbin/Combinatorics/Quiver.lean#L58,
where in the map field we need to write fun f => f rather than fun X Y f => f.

[dselsam]

Synport won't have type information in general. It might be easier to set_option hackport.disableImplicitLambda true on the Lean4 side and then (semi-auto) refactor once things type-check in Lean4.

[kim-em]

Just to make sure I understand, you're suggesting that we add this option in Lean 4 core?