diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index db9aaa22821c1a558468675a6624fe6fb7a7f6b7..81f316f5d022dd84745426a65040b009618109ca 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -425,8 +425,7 @@ Section proofmode_classes.
   Implicit Types e : expr Λ.
 
   Global Instance frame_wp p s E e R Φ Ψ :
-    (class_instances_frame.FrameNoInstantiateExist →
-     ∀ v, Frame p R (Φ v) (Ψ v)) →
+    (FrameNoInstantiateExist → ∀ v, Frame p R (Φ v) (Ψ v)) →
     Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}) | 2.
   Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR, I. Qed.
 
diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index d6e5ca3823193e83ebe619eab2c0375dfd47b81e..37fd6bb10d5a6ab4c9cd3b26af5be194c7ab31cf 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -196,11 +196,6 @@ Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
   MakeOr Q1 Q2 Q → Frame true R (P1 ∨ P2) Q | 9.
 Proof. rewrite /Frame /MakeOr => [[<-]] [<-] _ <-. by rewrite -sep_or_l. Qed.
 
-(* We want a way to disable instantiating quantifiers when we are
-framing beneath connectives like [∀], [-∗] and [→]. See iris#565. *)
-Class FrameNoInstantiateExist : Prop := frame_no_instantiate_exist : True.
-Notation FrameCanInstantiateExist := (TCUnless FrameNoInstantiateExist).
-
 Global Instance frame_wand p R P1 P2 Q2 :
   (FrameNoInstantiateExist → Frame p R P2 Q2) →
   Frame p R (P1 -∗ P2) (P1 -∗ Q2) | 2.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index d9e4f7a882767a6372d49ea8b812017b9851a77f..ad8818bb756231578ab69c13a7678b724c6200e0 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -397,6 +397,13 @@ For more details, see also iris!989 and the [frame_and] and [frame_or_spatial]
 instances in [class_instances_frame.v] *)
 Notation MaybeFrame p R P Q progress := (TCNoBackTrack (MaybeFrame' p R P Q progress)).
 
+(* The [iFrame] tactic is able to instantiate witnesses for existential
+quantifiers. We need a way to disable this behavior beneath connectives
+like [∀], [-∗] and [→], since it is often unwanted in these cases.
+Also see iris#565. *)
+Class FrameNoInstantiateExist : Prop := frame_no_instantiate_exist : True.
+Notation FrameCanInstantiateExist := (TCUnless FrameNoInstantiateExist).
+
 Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
 Global Arguments IntoExcept0 {_} _%I _%I : simpl never.
 Global Arguments into_except_0 {_} _%I _%I {_}.