Before, we often had to insert awkward casts when using them. Also,
the generality of also having them on Type, is probably not useful.

As suggested by Pierre-Marie Pédrot in the Coq-club thread:

  [Coq-Club] Very slow failing apply

To work arround some performance issues in Iris.

This is needed to use coq-stdpp in developments with -type-in-type
as set_unfold will otherwise unify with any hyp, causing the
set_solver tactic to break.

This way, we get more definitional equalities.