simplify telescope-based notations

These type annotations are no longer needed once we have a bidirectionality hint on tele_app.

Requires stdpp!342 (merged) and !763 (merged).