Improvement for 'auto'

Now proof search can be deferred if there are too many metavariables in
the goal - previously in this case it would happily pick any old
solution causing weird errors elsewhere in some cases.
Need to resolve autos in each 'try' branch

If the branch solves an implicit which makes the auto solvable, we need
to try to resolve it straight away so we know whether the branch is
valid or not. We need this especially when using 'try' to implement
implicit coercions.