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)).