Several leftovers of 403

[ice1000]

Several leftovers:

• [x] I still wish idiom brackets to be desugared in the desugarer, so (| 1 + 2 |) would work.
• [ ] It would be nice if LocalVar.IGNORED are generated for unused telescopes, but doing so fails the assertion. I think this might mean that we have substitution bugs (maybe we need to formalize everything like Idris2 did...).
• [ ] There isn't something like do(myBind, myReturn), and we don't have local openings. I guess we may want local openings.

Originally posted by @ice1000 in https://github.com/aya-prover/aya-dev/issues/403#issuecomment-1134983216

[ice1000]

I think it makes sense for now to improve the idiom brackets feature and push the others until we have time