This will not compile until @janno's stdpp fix is merged.
Old description
See explanation in #461 (comment 80771).
This allows the example to pass, but I don't know that this is the right change, and I don't understand the graph produced with this change.
Moreover, it might restore one annoyance that stdpp!368 (merged) complained about (not sure if this is still an annoyance):
In Iris, what this means is that
bi_tforall/bi_texisthave different universe levels thanbi_forall/bi_exist.
I suspect this overall lets bi_tforall/bi_texist take a tele@{U} for some fixed U such that U < bi.Quant. That might be okay, since nobody nests telescopes (else we'd have to make them universe-polymorphic, triggering issues elsewhere).