feat: iframe with existential quantifiers

[alvinylt]

Description

Implements iframe with support for framing existentially quantified propositions.

Addresses #390 and #400.

Similar to FrameInstantiateExistEnabled in the Rocq version, this feature can be disabled for specific proofs/instances using the option iris.frame.instantiateExists. In the following example, iframe frames HP and HS. Without the set_option iris.frame.instantiateExists false line, it would solve the goal entirely.

set_option iris.frame.instantiateExists false in
example [BI PROP] {α} (a : α) (P : PROP) (Q R : α → PROP) (S : PROP) :
    ⊢ P -∗ Q a -∗ R a -∗ S -∗ ∃ n, P ∗ Q n ∗ ∃ m, R m ∗ S := by
  iintro HP HQ HR HS
  iframe ∗

In the Rocq version, FrameInstantiateExistEnabled is used in frame_wand, frame_forall, frame_impl_persistent and frame_impl. The existing Lean counterparts of these four declarative type class instances are replaced by SynthTactic definitions so that the option iris.frame.instantiateExists can be set.

A caveat is that SynthTactic definitions have higher priority than declarative instances, while the instances frame_wand, frame_forall, frame_impl_persistent and frame_impl should have lower priority than frame_here. Now that they are defined as SynthTactic instances, we use the function frameHereApplies to specifically check whether frame_here is relevant and give priority to frame_here whenever possible.

We are using mkAppM instead of Qq in frameWp for similar reasons regarding IProp GF as in PR #510.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[MackieLoeffel]

@alvinylt I simplified the code in 0f9968b Please have a look if this looks correct to you. If yes, I think this is ready to merge.

Edit: Something seems to be wrong since CI fails. I will look into this. (fixed)

[alvinylt]

The simplification of solveGatherEvarsEq looks good to me 👍🏼

Regarding frame_texist and frame_tforall, I'm actually not so familiar with the various occurrences of telescopes in the code. In these two cases, telescopes refer to the defined in stdpp. But there is also bi/telescopes.v which is yet to be ported. Is it a Rocq-specific feature? Should add_modal_tforall in #500 also be ignored?