Use withExpandLast to not turn implicit args at the end into metavariables

[L-TChen]

For the use of this function, see https://agda.readthedocs.io/en/latest/language/reflection.html#type-checking-computations.

If implicit parameters or arguments appear at the end, then they would be turned into metavariables before explicitly giving arguments. I don't have a minimal working example for now, though.