implicit arguments in quotient.v, close #447