Yes – for anyone who wants their proof states to be legible. I always recommend it to students. It’s exactly the same principle as having [_,_,_] for lists instead of _::_::_::nil. Larry > On 10 Oct 2024, at 19:16, Makarius <makarius at sketis.net> wrote: > > Are there any remaining uses of show_brackets?