Add an optional depth to 'search' tactic

Also add it to Language.Reflection.  It's now good enough to work with
the proof obligations in Effects, so replace the old proof search (it's
also noticeably faster in larger programs).

Requires ibcs to be rebuilt.