MVarId.apply without infering instance arguments

Stream: metaprogramming / tactics

[Liam Schilling]

Hello,

Is there a way to get similar functionality to MVarId.apply e but which does not even try to synthesize the BinderInfo.instImplicit arguments of e, instead treating them all exactly as though they just had the BinderInfo.default binding? That is, returning them as subgoals.