I think this also fixes #146 (closed) by using typeclasses eauto instead of apply _.
typeclasses eauto
apply _