implicit arguments in quotient.v, close #447

Minor, non-blocking point: I think this would be better as a Local Notation, so we don't have a quotient := @quotient sR showing up in the proof terms.