Wingman can't run "introduce lambda" on impredicative holes #1571
Description
The call to isFunction fails on impredicative holes, resulting in the Introduce lambda code action not appearing, and the intros tactic making no progress. The ctxDefiningFuncs has a corresponding polytype that we can use instead, but it's non-trivial to determine if we've already bound any arguments.