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.

Conflicts:
	opam.pins

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...).

Conflicts:
	_CoqProject
	theories/typing/tests/get_x.v
	theories/typing/tests/unbox.v