Use syntactic sugar for useless binders in pretty-printer.
Use syntactic sugar for useless binders in pretty-printer.

Now, degenerate pi-types show up as arrows, degenerate sigmas as products, and
degenerate dependent pairs as ordinary pairs.

david-christiansen/tiny-dependent-types