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