This PR adds syntax for lambda arguments to combinators:

OR.on_range_weaken f g i j
  fn k { rewrite f k as g k }

Which used to be:

ghost
fn weaken (k:nat { i <= k /\ k < j })
requires f k
ensures g k
{
  rewrite (f k) as (g k)
};
OR.on_range_weaken f g i j weaken

Limitations/notes:

• Only final arguments are supported. (So no lambdas in record fields.)
• Only arguments to stt(ghost/atomic) functions are supported. (So no record constructors.)
• The type of the lambda needs to be inferable from the arguments alone, not the slprops in the contexts. (The matcher is run after declaring the auxiliary functions.)
• Under the hood this compiles down to a nested auxiliary function like we used to write. We add an extra unit argument to prevent ANF from kicking in.

I've also added a cute generic introduction function for forall/trade/shift/etc.:

intro (forall* l. is_list x l @==> is_list x ([] @ l)) fn _ l {};