Boxes for function types are part of the function type itself and we do not need to add them everywhere.

This reverts commit 04386c1c.

For consistency with how we call this elsewhere in Iris.

Cleaning : remove hints about [product2] from solve_typing (this type is only for internal use), and removed unnecessary unfold lemmas.

Typechecked lazy lifetime initialization. Also, switched from eauto to typeclasses eauto, which seems way less bugged (but I still found something strange...).

For some reason I have to fix some diverging proof scripts

Coq's module system is wholly inadequate :/