Ltac typeclass_instantiation := eauto 50 with typeclass_instances || eauto.