Pick and name universes for [bi_tforall] and [bi_texist].

This requires the [fixpoint] version of [tele_arg].

iris/bi/bi.v

@@ -3,6 +3,12 @@ From iris.bi Require Export updates internal_eq plainly embedding.
 From iris.prelude Require Import options.
 
 Module Import bi.
+  (** Get universes into the desired scope *)
+  Universe Logic.
+  Constraint Logic = bi.interface.universes.Logic.
+  Universe Quant.
+  Constraint Quant = bi.interface.universes.Quant.
+  (** Get other symbols into the desired scope *)
   Export bi.interface.bi.
   Export bi.derived_laws.bi.
   Export bi.derived_laws_later.bi.

iris/bi/interface.v

@@ -164,8 +164,15 @@ Section bi_mixin.
   Qed.
 End bi_mixin.
 
+Module Import universes.
+  (** The universe of the logic (PROP). *)
+  Universe Logic.
+  (** The universe of quantifiers in the logic. *)
+  Universe Quant.
+End universes.
+
 Structure bi := Bi {
-  bi_car :> Type;
+  bi_car :> Type@{Logic};
   bi_dist : Dist bi_car;
   bi_equiv : Equiv bi_car;
   bi_entails : bi_car → bi_car → Prop;
@@ -174,8 +181,8 @@ Structure bi := Bi {
   bi_and : bi_car → bi_car → bi_car;
   bi_or : bi_car → bi_car → bi_car;
   bi_impl : bi_car → bi_car → bi_car;
-  bi_forall : ∀ A, (A → bi_car) → bi_car;
-  bi_exist : ∀ A, (A → bi_car) → bi_car;
+  bi_forall : ∀ A : Type@{Quant}, (A → bi_car) → bi_car;
+  bi_exist : ∀ A : Type@{Quant}, (A → bi_car) → bi_car;
   bi_sep : bi_car → bi_car → bi_car;
   bi_wand : bi_car → bi_car → bi_car;
   bi_persistently : bi_car → bi_car;

iris/bi/telescopes.v

@@ -6,10 +6,10 @@ Import bi.
 (* This cannot import the proofmode because it is imported by the proofmode! *)
 
 (** Telescopic quantifiers *)
-Definition bi_texist {PROP : bi} {TT : tele} (Ψ : TT → PROP) : PROP :=
+Definition bi_texist {PROP : bi} {TT : tele@{Quant}} (Ψ : TT → PROP) : PROP :=
   tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
 Global Arguments bi_texist {_ !_} _ /.
-Definition bi_tforall {PROP : bi} {TT : tele} (Ψ : TT → PROP) : PROP :=
+Definition bi_tforall {PROP : bi} {TT : tele@{Quant}} (Ψ : TT → PROP) : PROP :=
   tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
 Global Arguments bi_tforall {_ !_} _ /.
 
@@ -21,7 +21,7 @@ Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) ..
   format "∀..  x  ..  y ,  P") : bi_scope.
 
 Section telescopes.
-  Context {PROP : bi} {TT : tele}.
+  Context {PROP : bi} {TT : tele@{Quant}}.
   Implicit Types Ψ : TT → PROP.
 
   Lemma bi_tforall_forall Ψ : bi_tforall Ψ ⊣⊢ bi_forall Ψ.
@@ -34,7 +34,7 @@ Section telescopes.
     - simpl. apply (anti_symm _); apply forall_intro; intros a.
       + rewrite /= -IH. apply forall_intro; intros p.
         by rewrite (forall_elim (TargS a p)).
-      + move/tele_arg_inv : (a) => [x [pf ->]] {a} /=.
+      + destruct a=> /=.
         setoid_rewrite <- IH.
         rewrite 2!forall_elim. done.
   Qed.
@@ -47,7 +47,7 @@ Section telescopes.
         rewrite (tele_arg_O_inv p) //.
       + by rewrite -(exist_intro TargO).
     - simpl. apply (anti_symm _); apply exist_elim.
-      + intros p. move/tele_arg_inv: (p) => [x [pf ->]] {p} /=.
+      + intros p. destruct p => /=.
         by rewrite -exist_intro -IH -exist_intro.
       + intros x.
         rewrite /= -IH. apply exist_elim; intros p.

tests/telescopes.v

@@ -176,3 +176,7 @@ Restart.
 Abort.
 
 End telescopes_and_tactics.
+
+Lemma tele_universe {PROP : bi} (TT : tele@{bi.Quant}) (P : TT → PROP) :
+  bi_texist P ⊣⊢ bi_exist P.
+Proof. apply bi_texist_exist. Qed.