Add testcase for #461

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_texist have different universe levels than bi_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).