Improve `iFrame` to instantiate existential quantifiers

This MR enables iFrame to instantiate existential quantifiers. For example:

Lemma test_iFrame_exists_instantiate (Φ Ψ : nat → PROP) P Q :
  P ∗ Φ 0 ∗ Ψ 1 ∗ Q ⊢ ∃ n, Φ n ∗ ∃ m, Ψ m ∗ P ∗ Q.
Proof.
  iIntros "(HP & HΦ & HΨ & HQ)".
  iFrame "HΨ". (* instantiates the inner existential quantifier [m] *)
  iFrame "HP". (* keeps the outer existential quantifier [n] around *)
  iFrame "HΦ". (* instantiates the outer existential quantifier [n] *)
  done.
Qed.

The tricky part of this functionality is achieving acceptable performance. A naive implementation with two Frame instances (one to instantiate, one to keep the quantifier around) would need to check 2^n possibilities for n quantifiers.

This MR circumvents that: it uses a more general lemma for Frameing under existentials, which allows us to defer making this choice.
Suppose we want to find a frame instance Frame P (∃ a, Φ a) ?R (~= P ∗ R ⊢ ∃ a, Φ a, and we wish to compute R).
Operationally, this MR does the following:

• Run typeclass search for Frame P (Φ ?a) ?R', with ?a an evar. If this fails, we quit.
• If a has been unified with a concrete term, the remaining goal R is just R'
• If a remains an evar, the remaining goal R will be ∃ a, R'.

The approach in the code is a bit more general---it will find all the freshly generated evars occurring in a, and turn these back into existential quantifiers.

The MR currently removes support for framing existential quantifiers that occur beneath definitions. This can be fixed, but it would be good to discuss if this should be default behavior.

I discussed and showed this to some people at the Iris workshop. I've tried to simplify the code a bit since then. !989 (merged) was also needed to ensure this MR behaves well.