Non-dependent products optimisation

It could be interesting to store in the header of term whether it corresponds to a dependent Prod or not. As always, it would be stored as a OnceCell, as an overapproximation, typically determined:

• when building a term;
• when creating a term from within the kernel
• when performing a term substitution.

This would allow:

• to easily perform substitution, typically during beta-reduction, as the resulting type of a well-typed beta-reduction could be found instantly (this could overlap with the is_certainly_closed header data, but I believe a is_certainly_non_dependent header data could be what we really want instead --- and both could also be kept)
• to ensure pretty printing (see #55) of the corresponding types. I believe there is no need to implement a potential "skeleton" as described #65 just now.