generalize quotient-of-kernel factorization into quotient.v

This is a general fact about quotients of kernels.
Why is this now commented out?