diff --git a/tests/proofmode.v b/tests/proofmode.v
index f4194381ed575916223d678e3ef8bddec8162880..9194db0b7f8de8952bbe7480443ee2ce87ea1923 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -109,6 +109,10 @@ Lemma test_very_fast_iIntros P :
   ∀ x y : nat, (⌜ x = y ⌝ → P -∗ P)%I.
 Proof. by iIntros. Qed.
 
+Definition tc_opaque_test : PROP := tc_opaque (∀ x : nat, ⌜ x = x ⌝)%I.
+Lemma test_iIntros_tc_opaque : tc_opaque_test.
+Proof. by iIntros (x). Qed.
+
 (** Prior to 0b84351c this used to loop, now `iAssumption` instantiates `R` with
 `False` and performs false elimination. *)
 Lemma test_iAssumption_evar_ex_false : ∃ R, R ⊢ ∀ P, P.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index a294222f0e37b9ce071557d3297c10e82ed14874..a71e3527760550471e291c74be94512c03aaf9ec 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -619,6 +619,8 @@ Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   FromExist P Φ → FromExist (tc_opaque P) Φ := id.
 Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (tc_opaque P) Φ := id.
+Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
+  FromForall P Φ → FromForall (tc_opaque P) Φ := id.
 Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
 Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}