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