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