Underline seems like a perfectly sensible thing to me. I've run into problems like his "same Γ, different x and τ" example many times. In PLT Redex, I have to either make sure the thing I intend to be non-subscripted is already bound elsewhere or make an after-the-fact check that all of the subscripted versions of it are equal. Both options are awkward, and which one I have to do varies by situation. An `unsequence' notation to complement the `sequence' notation (which is actually done in Redex by appending an ellipsis) would let me directly say what I mean. The OCR issue is strictly an aspect of the marks put on the page rather than the ideas they describe, and a completely serial notation could be used as well (similar to backtick and comma for quasiquotation).