Instantiation Tactic := eauto 50 with typeclass_instances || eauto.