feat: add `instantiateRevBetaS`

This PR implements `instantiateRevBetaS` which is similar to
`instantiateRevS`, but beta-reduces nested applications whose function
becomes a lambda after substitution.

For example, if `e` contains a subterm `#0 a` and we apply the substitution `#0 := fun x => x + 1`,
then `instantiateRevBetaS` produces `a + 1` instead of `(fun x => x + 1) a`.

This is useful when applying theorems. For example, when applying `Exists.intro`:
```lean
Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p
```
to a goal of the form `∃ x : Nat, p x ∧ q x`, we create metavariables `?w` and `?h`.
With `instantiateRevBetaS`, the type of `?h` becomes `p ?w ∧ q ?w` instead of
`(fun x => p x ∧ q x) ?w`.