generalize quotient-of-kernel factorization into quotient.v

This is a general fact about quotients of kernels.
In this case that seems OK. However, I had some horrible instances in
`corn` where type classes instance search changed.
We should try not to be too clever with type classes, or `eauto` for that
matter.
Sorry if this is in some way confirming what @andrejbauer said.




On Fri, Sep 5, 2014 at 7:26 AM, Mike Shulman <notifications@github.com>
wrote:

> In theories/hit/V.v:
>
> >
> > +(* Instance ismere_ker_bisim {A} (f : A -> V) : is_mere_relation (ker_bisim f). *)
>
> I commented it out to see whether it was necessary, but then forgot to
> remove it entirely. It's unnecessary because typeclass resolution can
> generate this instance automatically.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/460/files#r17157355>.
>