Allow numerals in projections.
Coq-style printing of products.
Bug in synthesizing the type of a projection.
Example: propositional truncation and interval.

It’s kind of surprising that once the computation rules for truncation
and booleans are installed as rewrites we don’t need any equality hints
or new rewrite hints.