Pretty printing of terms

One may see the kernel space as a quotient space. Indeed, the kernel treat certain terms equally, even though from a user perspective they have different names, locations, etc. This is of course done on purpose, but it means a naive printing of terms can only display a plain de Bruijn term, which is increasingly impractical to read as the size of the term grows.

The suggested enhancements are the following:

• print terms with classic identifier (as opposed to de Bruijn's), preferably letters;
• be able to omit certain pairs of parentheses;
• print non-dependent arrow type as A -> B instead of (_: A) -> B;
• print dependent arrow types with an output type of type Prop as ∀x: A. B instead of (x: A) -> B;

Some of these are already implemented by !59 (merged). Note that, for the third suggestion, it might be useful to have a clear notion of skeletons, as defined in #65. Indeed, knowing the skeleton of a term T w.r.t. to a given variable n indicates whether T depends on n, which can tell whether a given product type is dependent or not.