add Coq typeclass index problem draft