diff --git a/CHANGELOG.md b/CHANGELOG.md
index a9da76d1e2e592994e3a5f162ec7b67675e341ef..6e00c253c7298f275699d8b5c9275b5c1703f5d7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -91,6 +91,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Rename `{o,r,ur}Functor_{ne,id,compose,contractive}` into
   `{o,r,ur}Functor_map_{ne,id,compose,contractive}`.
 * Add `{o,r,ur}Functor_oFunctor_compose` for composition of functors.
+* Affine, absorbing, persistent and timeless instances for telescopes.
+* Better support for telescopes in the proof mode, i.e., all tactics should
+  recognize and distribute telescopes now.
 
 **Changes in heap_lang:**
 
diff --git a/tests/telescopes.v b/tests/telescopes.v
index a60ba91e0b76ab12b315b3c5995c395f63377d7d..401458967b8721101ef92d10f2ea5f81ff956c9e 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -2,6 +2,57 @@ From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
+Section basic_tests.
+  Context {PROP : sbi}.
+  Implicit Types P Q R : PROP.
+
+  Lemma test_iIntros_tforall {TT : tele} (Φ : TT → PROP) :
+    ⊢ ∀.. x, Φ x -∗ Φ x.
+  Proof. iIntros (x) "H". done. Qed.
+  Lemma test_iPoseProof_tforall {TT : tele} P (Φ : TT → PROP) :
+    (∀.. x, P ⊢ Φ x) → P -∗ ∀.. x, Φ x.
+  Proof.
+    iIntros (H1) "H2"; iIntros (x).
+    iPoseProof (H1) as "H1". by iApply "H1".
+  Qed.
+  Lemma test_iApply_tforall {TT : tele} P (Φ : TT → PROP) :
+    (∀.. x, P -∗ Φ x) -∗ P -∗ ∀.. x, Φ x.
+  Proof. iIntros "H1 H2" (x). by iApply "H1". Qed.
+  Lemma test_iAssumption_tforall {TT : tele} (Φ : TT → PROP) :
+    (∀.. x, Φ x) -∗ ∀.. x, Φ x.
+  Proof. iIntros "H" (x). iAssumption. Qed.
+  Lemma test_pure_texist {TT : tele} (φ : TT → Prop) :
+    (∃.. x, ⌜ φ x ⌝) -∗ ∃.. x, ⌜ φ x ⌝ : PROP.
+  Proof. iIntros (H) "!%". done. Qed.
+  Lemma test_pure_tforall {TT : tele} (φ : TT → Prop) :
+    (∀.. x, ⌜ φ x ⌝) -∗ ∀.. x, ⌜ φ x ⌝ : PROP.
+  Proof. iIntros (H) "!%". done. Qed.
+  Lemma test_pure_tforall_persistent {TT : tele} (Φ : TT → PROP) :
+    (∀.. x, <pers> (Φ x)) -∗ <pers> ∀.. x, Φ x.
+  Proof. iIntros "#H !#" (x). done. Qed.
+  Lemma test_pure_texists_intuitionistic {TT : tele} (Φ : TT → PROP) :
+    (∃.. x, □ (Φ x)) -∗ □ ∃.. x, Φ x.
+  Proof. iDestruct 1 as (x) "#H". iExists (x). done. Qed.
+  Lemma test_iMod_tforall {TT : tele} P (Φ : TT → PROP) :
+    ◇ P -∗ (∀.. x, Φ x) -∗ ∀.. x, ◇ (P ∗ Φ x).
+  Proof. iIntros ">H1 H2" (x) "!> {$H1}". done. Qed.
+  Lemma test_timeless_tforall {TT : tele} (φ : TT → Prop) :
+    ▷ (∀.. x, ⌜ φ x ⌝) -∗ ◇ ∀.. x, ⌜ φ x ⌝ : PROP.
+  Proof. iIntros ">H1 !>". done. Qed.
+  Lemma test_timeless_texist {TT : tele} (φ : TT → Prop) :
+    ▷ (∃.. x, ⌜ φ x ⌝) -∗ ◇ ∃.. x, ⌜ φ x ⌝ : PROP.
+  Proof. iIntros ">H1 !>". done. Qed.
+  Lemma test_add_model_texist `{!BiBUpd PROP} {TT : tele} P Q (Φ : TT → PROP) :
+    (|==> P) -∗ (P -∗ Q) -∗ ∀.. x, |==> Q ∗ (Φ x -∗ Φ x).
+  Proof. iIntros "H1 H2". iDestruct ("H2" with "[> $H1]") as "$". auto. Qed.
+  Lemma test_iFrame_tforall {TT : tele} P (Φ : TT → PROP) :
+    P -∗ ∀.. x, P ∗ (Φ x -∗ Φ x).
+  Proof. iIntros "$". auto. Qed.
+  Lemma test_iFrame_texist {TT : tele} P (Φ : TT → PROP) :
+    P -∗ (∃.. x, Φ x) -∗ ∃.. x, P ∗ Φ x.
+  Proof. iIntros "$". auto. Qed.
+End basic_tests.
+
 Section accessor.
 (* Just playing around a bit with a telescope version
    of accessors with just one binder list. *)
diff --git a/theories/bi/telescopes.v b/theories/bi/telescopes.v
index d54533929a945c82d8872083527dacbaaff6251c..5a9051edff2da7bbd2a7912899d3a6a6dd0d33b0 100644
--- a/theories/bi/telescopes.v
+++ b/theories/bi/telescopes.v
@@ -20,11 +20,11 @@ Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) ..
   (at level 200, x binder, y binder, right associativity,
   format "∀..  x  ..  y ,  P") : bi_scope.
 
-Section telescope_quantifiers.
+Section telescopes_bi.
   Context {PROP : bi} {TT : tele}.
+  Implicit Types Ψ : TT → PROP.
 
-  Lemma bi_tforall_forall (Ψ : TT → PROP) :
-    bi_tforall Ψ ⊣⊢ bi_forall Ψ.
+  Lemma bi_tforall_forall Ψ : bi_tforall Ψ ⊣⊢ bi_forall Ψ.
   Proof.
     symmetry. unfold bi_tforall. induction TT as [|X ft IH].
     - simpl. apply (anti_symm _).
@@ -39,8 +39,7 @@ Section telescope_quantifiers.
         rewrite 2!forall_elim. done.
   Qed.
 
-  Lemma bi_texist_exist (Ψ : TT → PROP) :
-    bi_texist Ψ ⊣⊢ bi_exist Ψ.
+  Lemma bi_texist_exist Ψ : bi_texist Ψ ⊣⊢ bi_exist Ψ.
   Proof.
     symmetry. unfold bi_texist. induction TT as [|X ft IH].
     - simpl. apply (anti_symm _).
@@ -57,26 +56,45 @@ Section telescope_quantifiers.
 
   Global Instance bi_tforall_ne n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_tforall PROP TT).
-  Proof.
-    intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
-  Qed.
-
+  Proof. intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //. Qed.
   Global Instance bi_tforall_proper :
     Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_tforall PROP TT).
-  Proof.
-    intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
-  Qed.
+  Proof. intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //. Qed.
 
   Global Instance bi_texist_ne n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_texist PROP TT).
-  Proof.
-    intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
-  Qed.
-
+  Proof. intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //. Qed.
   Global Instance bi_texist_proper :
     Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_texist PROP TT).
-  Proof.
-    intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
-  Qed.
+  Proof. intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //. Qed.
+
+  Global Instance bi_tforall_absorbing Ψ :
+    (∀ x, Absorbing (Ψ x)) → Absorbing (∀.. x, Ψ x).
+  Proof. rewrite bi_tforall_forall. apply _. Qed.
+  Global Instance bi_tforall_persistent Ψ :
+    (∀ x, Persistent (Ψ x)) → Persistent (∀.. x, Ψ x).
+  Proof. rewrite bi_tforall_forall. apply _. Qed.
+
+  Global Instance bi_texist_affine Ψ :
+    (∀ x, Affine (Ψ x)) → Affine (∃.. x, Ψ x).
+  Proof. rewrite bi_texist_exist. apply _. Qed.
+  Global Instance bi_texist_absorbing Ψ :
+    (∀ x, Absorbing (Ψ x)) → Absorbing (∃.. x, Ψ x).
+  Proof. rewrite bi_texist_exist. apply _. Qed.
+  Global Instance bi_texist_persistent Ψ :
+    (∀ x, Persistent (Ψ x)) → Persistent (∃.. x, Ψ x).
+  Proof. rewrite bi_texist_exist. apply _. Qed.
+End telescopes_bi.
+
+Section telescopes_sbi.
+  Context {PROP : sbi} {TT : tele}.
+  Implicit Types Ψ : TT → PROP.
+
+  Global Instance bi_tforall_timeless Ψ :
+    (∀ x, Timeless (Ψ x)) → Timeless (∀.. x, Ψ x).
+  Proof. rewrite bi_tforall_forall. apply _. Qed.
 
-End telescope_quantifiers.
+  Global Instance bi_texist_timeless Ψ :
+    (∀ x, Timeless (Ψ x)) → Timeless (∃.. x, Ψ x).
+  Proof. rewrite bi_texist_exist. apply _. Qed.
+End telescopes_sbi.
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 3edfef488945525fd1c36916a1aa44dcca62e9ae..30f3d187957a5ffd587f672309bac73a26edaf91 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -45,6 +45,12 @@ Proof.
   - apply bi.forall_intro=>?. apply H1, H2.
   - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
 Qed.
+Global Instance as_emp_valid_tforall {TT : tele} (φ : TT → Prop) (P : TT → PROP) :
+  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀.. x, φ x) (∀.. x, P x).
+Proof.
+  rewrite /AsEmpValid !tforall_forall bi_tforall_forall.
+  apply as_emp_valid_forall.
+Qed.
 
 (* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
    sure this instance is not used when there is no embedding between
@@ -142,6 +148,12 @@ Proof.
   rewrite /KnownLFromAssumption /FromAssumption=> <-.
   by rewrite forall_elim.
 Qed.
+Global Instance from_assumption_tforall {TT : tele} p (Φ : TT → PROP) Q x :
+  FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀.. x, Φ x) Q.
+Proof.
+  rewrite /KnownLFromAssumption /FromAssumption=> <-.
+  by rewrite bi_tforall_forall forall_elim.
+Qed.
 
 Global Instance from_assumption_bupd `{BiBUpd PROP} p P Q :
   FromAssumption p P Q → KnownRFromAssumption p P (|==> Q).
@@ -164,9 +176,17 @@ Proof. rewrite /FromPure /IntoPure pure_impl=> <- -> //. Qed.
 Global Instance into_pure_exist {A} (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃ x, Φ x) (∃ x, φ x).
 Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
+Global Instance into_pure_texist {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
+  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃.. x, Φ x) (∃.. x, φ x).
+Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.
 Global Instance into_pure_forall {A} (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀ x, Φ x) (∀ x, φ x).
 Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.
+Global Instance into_pure_tforall {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
+  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀.. x, Φ x) (∀.. x, φ x).
+Proof.
+  rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
+Qed.
 
 Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∗ P2) (φ1 ∧ φ2).
@@ -225,12 +245,20 @@ Proof.
   rewrite /FromPure=>Hx. rewrite pure_exist affinely_if_exist.
   by setoid_rewrite Hx.
 Qed.
+Global Instance from_pure_texist {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
+  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∃.. x, Φ x) (∃.. x, φ x).
+Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qed.
 Global Instance from_pure_forall {A} a (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀ x, Φ x) (∀ x, φ x).
 Proof.
   rewrite /FromPure=>Hx. rewrite pure_forall. setoid_rewrite <-Hx.
   destruct a=>//=. apply affinely_forall.
 Qed.
+Global Instance from_pure_tforall {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
+  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀.. x, Φ x) (∀.. x, φ x).
+Proof.
+  rewrite /FromPure !tforall_forall bi_tforall_forall. apply from_pure_forall.
+Qed.
 
 Global Instance from_pure_pure_sep_true a1 a2 (φ1 φ2 : Prop) P1 P2 :
   FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
@@ -434,8 +462,7 @@ Qed.
 Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
   IntoWand p q (Φ x) P Q → IntoWand p q (∀ x, Φ x) P Q.
 Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
-
-Global Instance into_wand_tforall {A} p q (Φ : tele_arg A → PROP) P Q x :
+Global Instance into_wand_tforall {TT : tele} p q (Φ : TT → PROP) P Q x :
   IntoWand p q (Φ x) P Q → IntoWand p q (∀.. x, Φ x) P Q.
 Proof. rewrite /IntoWand=> <-. by rewrite bi_tforall_forall (forall_elim x). Qed.
 
@@ -882,7 +909,7 @@ Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
 Proof. by rewrite /IntoOr -embed_or => <-. Qed.
 
 (** FromExist *)
-Global Instance from_exist_texist {A} (Φ : tele_arg A → PROP) :
+Global Instance from_exist_texist {TT : tele} (Φ : TT → PROP) :
   FromExist (∃.. a, Φ a) Φ.
 Proof. by rewrite /FromExist bi_texist_exist. Qed.
 Global Instance from_exist_pure {A} (φ : A → Prop) :
@@ -913,7 +940,7 @@ Qed.
 (** IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
 Proof. by rewrite /IntoExist. Qed.
-Global Instance into_exist_texist {A} (Φ : tele_arg A → PROP) :
+Global Instance into_exist_texist {TT : tele} (Φ : TT → PROP) :
   IntoExist (∃.. a, Φ a) Φ | 10.
 Proof. by rewrite /IntoExist bi_texist_exist. Qed.
 Global Instance into_exist_pure {A} (φ : A → Prop) :
@@ -951,7 +978,7 @@ Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
 (** IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
 Proof. by rewrite /IntoForall. Qed.
-Global Instance into_forall_tforall {A} (Φ : tele_arg A → PROP) :
+Global Instance into_forall_tforall {TT : tele} (Φ : TT → PROP) :
   IntoForall (∀.. a, Φ a) Φ | 10.
 Proof. by rewrite /IntoForall bi_tforall_forall. Qed.
 Global Instance into_forall_affinely {A} P (Φ : A → PROP) :
@@ -999,12 +1026,15 @@ Qed.
 Global Instance from_forall_forall {A} (Φ : A → PROP) :
   FromForall (∀ x, Φ x) Φ.
 Proof. by rewrite /FromForall. Qed.
-Global Instance from_forall_tforall {A} (Φ : tele_arg A → PROP) :
-  FromForall (∀.. x, Φ x)%I Φ.
+Global Instance from_forall_tforall {TT : tele} (Φ : TT → PROP) :
+  FromForall (∀.. x, Φ x) Φ.
 Proof. by rewrite /FromForall bi_tforall_forall. Qed.
 Global Instance from_forall_pure {A} (φ : A → Prop) :
   @FromForall PROP A ⌜∀ a : A, φ a⌝ (λ a, ⌜ φ a ⌝)%I.
 Proof. by rewrite /FromForall pure_forall. Qed.
+Global Instance from_tforall_pure {TT : tele} (φ : TT → Prop) :
+  @FromForall PROP TT ⌜∀.. x : TT, φ x⌝ (λ x, ⌜ φ x ⌝)%I.
+Proof. by rewrite /FromForall tforall_forall pure_forall. Qed.
 Global Instance from_forall_pure_not (φ : Prop) :
   @FromForall PROP φ ⌜¬ φ⌝ (λ a : φ, False)%I.
 Proof. by rewrite /FromForall pure_forall. Qed.
@@ -1052,10 +1082,15 @@ Global Instance elim_modal_wandM φ p p' P P' Q Q' mR :
   ElimModal φ p p' P P' (mR -∗? Q) (mR -∗? Q').
 Proof. rewrite /ElimModal !wandM_sound. exact: elim_modal_wand. Qed.
 Global Instance elim_modal_forall {A} φ p p' P P' (Φ Ψ : A → PROP) :
-  (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) → ElimModal φ p p' P P' (∀ x, Φ x) (∀ x, Ψ x).
+  (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) →
+  ElimModal φ p p' P P' (∀ x, Φ x) (∀ x, Ψ x).
 Proof.
   rewrite /ElimModal=> H ?. apply forall_intro=> a. rewrite (forall_elim a); auto.
 Qed.
+Global Instance elim_modal_tforall {TT : tele} φ p p' P P' (Φ Ψ : TT → PROP) :
+  (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) →
+  ElimModal φ p p' P P' (∀.. x, Φ x) (∀.. x, Ψ x).
+Proof. rewrite /ElimModal !bi_tforall_forall. apply elim_modal_forall. Qed.
 Global Instance elim_modal_absorbingly_here p P Q :
   Absorbing Q → ElimModal True p false (<absorb> P) P Q Q.
 Proof.
@@ -1096,6 +1131,9 @@ Global Instance add_modal_forall {A} P P' (Φ : A → PROP) :
 Proof.
   rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
+Global Instance add_modal_tforall {TT : tele} P P' (Φ : TT → PROP) :
+  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀.. x, Φ x).
+Proof. rewrite /AddModal bi_tforall_forall. apply add_modal_forall. Qed.
 Global Instance add_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
        (P P' : PROP') (Q : PROP) :
   AddModal P P' (|==> ⎡Q⎤)%I → AddModal P P' ⎡|==> Q⎤.
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/frame_instances.v b/theories/proofmode/frame_instances.v
index 696da901b497773f5618aa74be9565209b537222..1399b4c6085475d6504cb97c4f57a0250359af1e 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -1,5 +1,5 @@
 From stdpp Require Import nat_cancel.
-From iris.bi Require Import bi tactics.
+From iris.bi Require Import bi tactics telescopes.
 From iris.proofmode Require Import classes.
 Set Default Proof Using "Type".
 Import bi.
@@ -265,9 +265,15 @@ Qed.
 Global Instance frame_exist {A} p R (Φ Ψ : A → PROP) :
   (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∃ x, Φ x) (∃ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
+Global Instance frame_texist {TT : tele} p R (Φ Ψ : TT → PROP) :
+  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∃.. x, Φ x) (∃.. x, Ψ x).
+Proof. rewrite /Frame !bi_texist_exist. apply frame_exist. Qed.
 Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
   (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
+Global Instance frame_tforall {TT : tele} p R (Φ Ψ : TT → PROP) :
+  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∀.. x, Φ x) (∀.. x, Ψ x).
+Proof. rewrite /Frame !bi_tforall_forall. apply frame_forall. Qed.
 
 Global Instance frame_impl_persistent R P1 P2 Q2 :
   Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2).
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 _ _ _)].