Define [tele_arg] as a fixpoint

The current definition of tele_arg increases the universe level in a way that is unfortunate. In particular,

Inductive tele_arg : tele@{u} -> Type@{u+1} :=
| ...

In Iris, what this means is that bi_tforall/bi_texist have different universe levels than bi_forall/bi_exist. This MR re-defines tele_arg as a fixpoint, which prevents the universe bump. In particular:

Fixpoint tele_arg (t : tele@{u}) : Type@{u} :=
  ...

With this definition, the universes for the telescopic quantifiers can match the universes of the non-telescopic quantifiers in iris (this enables a separate MR to iris: iris!781 (merged)).

tests/telescopes.v

@@ -41,3 +41,14 @@ Notation "'[TEST'  x .. z ,  P ']'" :=
         (tele_app (λ x, .. (λ z, P) ..)))
   (x binder, z binder).
 Check [TEST (x y : nat), x = y].
+
+(** [tele_arg t] should live at the same universe
+as the types inside of [t] because [tele_arg t]
+is essentially just a (dependent) product.
+ *)
+Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
+
+(** This test would fail without [Unset Universe Minimization ToSet] in [telescopes.v]. *)
+Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) → Prop) :
+  texist P ↔ ex P.
+Proof. by rewrite texist_exist. Qed.