This would make the syntax less visually overwhelming, and may speed up the typechecker. An implementation is suggested [here](https://github.com/sinhp/groupoid_model_in_lean4/blob/f88038c3f216840dd68758f1709a37dbb3f4d935/GroupoidModel/Syntax/Synth.lean#L6).
