diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index d9613c1fedea5eb3417fd7028244f9799408cdc9..daea5a76008dad4940a9075262a88454c4fd101b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export bi.
+From iris.bi Require Export bi telescopes.
 From iris.bi Require Import tactics.
 From iris.proofmode Require Export base environments classes modality_instances.
 Set Default Proof Using "Type".
@@ -504,6 +504,9 @@ Proof. rewrite /IntoEmpValid => Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
 Lemma into_emp_valid_forall {A} (φ : A → Type) P x :
   IntoEmpValid (φ x) P → IntoEmpValid (∀ x : A, φ x) P.
 Proof. rewrite /IntoEmpValid => Hi1 Hi2. apply Hi1, Hi2. Defined.
+Lemma into_emp_valid_tforall {TT : tele} (φ : TT → Prop) P x :
+  IntoEmpValid (φ x) P → IntoEmpValid (∀.. x : TT, φ x) P.
+Proof. rewrite /IntoEmpValid tforall_forall=> Hi1 Hi2. apply Hi1, Hi2. Defined.
 Lemma into_emp_valid_proj φ P : IntoEmpValid φ P → φ → ⊢ P.
 Proof. intros HP. apply HP. Defined.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 30bbab30d5801e4a5fc6364c93d8f806520f1e01..7a5976c5b5fc184864598dca499577ac1724f3b5 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -785,6 +785,8 @@ Ltac iIntoEmpValid_go := first
      [(*goal for [φ] *)|iIntoEmpValid_go]
   |(* Case [∀ x : A, φ] *)
    notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
+  |(* Case [∀.. x : TT, φ] *)
+   notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
   |(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
    notypeclasses refine (into_emp_valid_here _ _ _)].