Wingman: Tactical support for deep recursion

[isovector]

This PR is a bit of a hodge-podge, sorry! It primarily removes the try and * tactic operators, replacing them with better functionality.

try has become a regular tactic, while * deserves to rot away. Instead, there is now nested which nests a function call into itself as many times as necessary to typecheck. This is the original motivation for *, but it never actually succeeded at that.

In order to get nested working, I needed to be able to work with unsaturated function applications (Wingman tries really hard to saturate everything, and then eta reduce everything before presenting it.) The application tactics now take a new Saturation parameter, letting you tweak how many unsaturated arguments they take, and there's a corresponding with_arg tactic to shift into an unsaturated context.

Finally, while playing with this stuff, I learned that freshTyvars didn't do what it said on the tin; it claims to instantiate forall tys, but instead it would just alpha rename them. So that's fixed now too!

---

The result of all this is that the metaprogramming language is now powerful enough to express "generically write fmap":

  intros f x
, homo x
; assumption      -- every term is either an assumption, or
| ( with_arg
  , assumption    -- some assumption that has been applied to
  , nested fmap   -- 0 or more nested fmaps
  , assume f      -- before calling f
  )